The problem of self-analytically choosing the set of support

This article is the seventh of a series of articles discussing various open research problems in automated reasoning. Here we focus on self-analysis and the set of support strategy. The problem proposed for research asks for one to find a means for an automated reasoning program to self-analytically determine which clauses to be in the set of support at various points during the program's attempt to complete a given assignment. For evaluating a proposed solution to this research problem, we include suggestions concerning possible test problems.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under contract W-31-109-Eng-38.     

The problem of guaranteeing the existence of a complete set of reductions

This article is the eleventh of a series of articles discussing various open research problems in automated reasoning. Here we focus on finding criteria for guaranteeing the existence of a complete set of reductions. We include a suggestion for evaluating a proposed solution to this research problem.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

The problem of guaranteeing the absence of a complete set of reductions

This article is the twelfth of a series of articles discussing various open research problems in automated reasoning. Here we focus on finding criteria for guaranteeing the absence of a complete set of reductions. We include a suggestion for evaluating a proposed solution to this research problem.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

The problem of finding a restriction strategy more effective than the set of support strategy

This article is the seventeenth of a series of articles discussing various open research problems in automated reasoning. Here we focus on formulating a new restriction strategy for curtailing the number of clauses generated and retained during the completion of an assignment. The problem proposed for research asks one to find a strategy that sharply restricts the tendency of an automated reasoning program to deduce far too many conclusions, many of which are redundant or irrelevant. The new strategy must be more powerful than the set of support strategy on a substantial set of problems. We suggest possible test problems from Tarskian geometry and the equivalential calculus for evaluating a proposed solution to this research problem.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

The problem of finding an inference rule for set theory

This article is the ninth of a series of articles discussing various open research problems in automated reasoning. Here we focus on finding an inference rule for set theory. The problem proposed for research asks one to find a means for building in set-theoretic reasoning in a manner similar to the way paramodulation builds in equality-oriented reasoning. For evaluating a proposed solution to this research problem, we include suggestions concerning possible test problems.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under contract W-31-109-Eng-38.     

The problem of choosing the representation,inference rule,and strategy

This article is the nineteenth of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks one to find guidelines for simultaneously choosing the most effective representation, inference rule, and strategy. Since the three areas are tightly coupled, formulation of such guidelines requires understanding the precise nature of this coupling. For evaluating a proposed solution to this research problem, we suggest possible test problems from group theory, Gödel's finite axiomatization of set theory, and program verification.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

The problem of definition expansion and contraction

This article is the fourth of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research focuses on finding criteria that would enable an automated reasoning program to expand or contract definitions wisely. For evaluating a proposed solution to this research problem, we include suggestions concerning possible test problems.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under contract W-31-109-Eng-38.     

The problem of demodulator adjunction

This article is the twenty-third of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks one to find criteria for deciding which e1uality unit clauses to adjoin with regard to CPU time and may affect refutation completeness. For evaluating a proposed solution to this research problem, we suggest problems from mathematics, logic, circuit design, program verification, and the world of puzzles.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract W     

The problem of finding a strategy to control binary paramodulation

This article is the fifth of a series of articles discussing various open research problems in automated reasoning. Here we focus on the equality relation which is so vital to many applications of automated reasoning. The prolem proposed for research asks one to find a strategy for controlling the application of binary paramodulation. For evaluating a proposed solution to this research problem, we include suggestions concerning possible test problems.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under contract W-31-109-Eng-38.     

The problem of choosing between logic programming and general-purpose automated reasoning

This article is the thirteenth of a series of articles discussing various open research problems in automated reasoning. Here we focus on finding criteria for correctly choosing between using logic programming and a more general automated reasoning approach to attack a given assignment. The problem proposed for research asks one to find criteria that classify problems as solvable with a well-focused algorithm or as requiring a more general search for new information. We include suggestions for evaluating a proposed solution to this research problem.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

An evaluation of buffer management strategies for relational database systems

In this paper we present a new algorithm, DBMIN, for managing the buffer pool of a relational database management system. DBMIN is based on a new model of relational query behavior, thequery locality set model (QLSM). Like the hot set model, the QLSM has an advantage over the stochastic models due to its ability to predict future reference behavior. However, the QLSM avoids the potential problems of the hot set model by separating the modeling of reference behavior from any particular buffer management algorithm. After introducing the QLSM and describing the DBMIN algorithm, we present a performance evaluation methodology for evaluating buffer management algorithms in a multiuser environment. This methodology employed a hybrid model that combines features of both trace-driven and distribution-driven simulation models. Using this model, the performance of the DBMIN algorithm in a multiuser environment is compared with that of the hot set algorithm and four more traditional buffer replacement algorithms.This research was partially supported by the Department of Energy under Contract No. DE-AC02-81ER10920 and the National Science Foundation under grant MCS82-01870.     

The problem of self-analytically choosing the weights

This article is the eighth of a series of articles discussing various open research problems in automated reasoning. Here we focus on self-analysis and the weighting strategy. The problem proposed for research asks one to find a means for an automated reasoning program to self-analytically determine which weights or priorities to give to clauses at various points during the program's attempt to complete a given assignment. For evaluating a proposed solution to this research problem, we include suggestions concerning possible test problems.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under contract W-31-109-Eng-38.     

A preview of the European Commission TELEMAN programme fortelerobotics research

TELEMAN was a programme of research and training for the European Atomic Energy Community under the Second and Third Framework Programmes in the field of remote handling in hazardous or disordered nuclear environments. The strategic objective was to develop advanced telerobots that respond to the needs of the nuclear industry, including maintenance, decommissioning and accident management. The emphasis was on improved nuclear safety through reducing the radiation exposure of human operators. The first set of 16 multi-partner contracts related to the development of components and sub-systems and their environmental tolerance. The second set of five projects integrated results from the first projects into research machines for demonstration, testing and evaluation in realistic conditions. The programme ended with the testing of the major TELEMAN research projects in industrial locations     

The problem of choosing the inference rule to employ

This article is the second of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research focuses on finding criteria or metarules for choosing the inference rule(s) to be employed by the automated reasoning program in use when instructing the program to complete a specific assignment. We include actual experiments that illustrate the difficulty of making an appropriate choice.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under contract W-31-109-Eng-38.     

The problem of choosing between predicate and function notation for problem representation

This article is the sixteenth of a series of articles discussing various open research problems in automated reasoning. Here we focus on choosing between the use of predicates and the use of functions for representing information to an automated reasoning program. The problem proposed for research asks one to find criteria that dictate the most effective choice of notation-functions or predicates-for presenting the question to be studied. The criteria must reflect the close coupling between inference rule, strategy, and representation. We suggest possible test problems for evaluating a proposed solution to this research problem.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

The problem of explaining the disparate performance of hyperresolution and paramodulation

This article is the sixth of a series of articles discussing various open research problems in automated reasoning. Here we focus on the effectiveness of hyperresolution versus that of paramodulation. The problem proposed for research asks one to find the properties that explain why paramodulation is so much more effective than hyperresolution is for solving various problems from algebra. Fore evaluating a proposed solution to this research problem, we include suggestions concerning possible test problems.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under contract W-31-109-Eng-38.     

The problem of choosing the type of subsumption to use

This article is the eighteenth of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks one to find criteria for choosing the type of subsumption (if any) to use for completing a specific assignment. Since subsumption can be expensive (in terms of computer time), the application of such criteria to select the most effective variant of subsumption for attacking a specific problem might materially affect the liklihood of success. As possible test problems for evaluating a proposed solution to this research problem, we suggest SAM's lemma, theorems from Tarskian geometry, and theorems from equivalential calculus.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

The problem of finding a mapping between clause representation and natural-deduction representation

This article is the fourteenth of a series of articles discussing various open research problems in automated reasoning. Here we focus on the relationship between two approaches to the automation of reasoning: the paradigm based on the clause language and that based on natural deduction. The problem proposed for research asks one to find a mapping between the two approaches such that reasoning programs based on either approach perform identically on a specific assignment. For evaluating a proposed solution to this research problem, we include suggestions concerning possible test problems.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

新型脉冲电源等效电路动态特性研究

研究电感储能的新型脉冲电源提高效能问题,采用脉冲电容储能型电源,制造复杂。采用开关控制,限制了发展,同时由于给出了脉冲电源的等效电路并导出电路对应的变系数微分方程,方程的解析求解较为复杂。为解决上述问题,建立了电感储能型等效电路的模型,进行仿真,结果明确了电路各元件参数对输出脉冲特性的影响,验证了计算结果的可靠性。研究电感储能型脉冲电源电路参数的取值对输出脉冲电压的特性有着较明显的控制效果,通过适当选择各元件参数的取值,可以获得较小脉冲电压脉宽的同时又有较高的电压幅度。仿真结果为新型脉冲电源系统设计过程中参数的选择提供了可靠的依据。     

浅谈石化行业仪表节能工作的开展

当前节能成为我国经济发展中的重要部分。随着我国节能工作的发展,各行各业节能意识不断增强。从仪表设计、选型、安装、维护、研究开发等方面融入节能理念,必然会成为今后仪表工作发展的一个方向,将会给企业带来潜在的巨大经济效益。本文阐述了仪表节能的途径和效果。