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 strategy and hyperresolution

This article is the thirty-first of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks one to find a strategy that can be coupled with the inference rule hyperresolution to control the behavior of an automated reasoning program as effectively as does paramodulation.This work was supported by the Office of Scientific Computing, 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 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 hyperparamodulation

This article is the thirty-second of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks one to find a variant of the inference rule hyperparamodulation that avoids generating many of the binary paramodulants ordinarily deduced.This work was supported by the Office of Scientific Computing, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

The problem of finding a semantic strategy for focusing inference rules

This article is the fifteenth of a series of articles discussing various open research problems in automated reasoning. Here we focus on finding a strategy — other than a simple syntactic one — that can be used for focusing the attention of the inference rule(s) in use. The problem proposed for research asks one to find semantic criteria for selecting the clauses needed to complete the application of an inference rule. Suggestions for test problems are included. We note that Yuan Yu has solved two of these problems using a rather different approach with the Boyer-Moore theorem prover; his work is reported elsewhere in this issue of the Journal of Automated Reasoning.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 selecting an approach based on prior success

This article is the twenty-sixth of a series of articles discussing various open research problems in automated reasoning. The problem posed for research asks one to find criteria for choosing from among previously answered questions a question that dictates the approach to take for attacking the problem of current interest. Especially because the better automated reasoning programs often offer a wide range of choices for representation, inference rule, and strategy, a solution to the proposed problem would materially reduce the difficulty of using these powerful aids for research.This work was supported by the Office of Scientific Computing, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

The problem of demodulation during inference rule application

This article is the twenty-second 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 when to permit and when to avoid demodulation during the application of inference rules, focusing mainly on hyperresolution, UR-resolution, and hyperparamodulation. Since these three inference rules admit natural points at which one or more demodulators (rewrite rules) could be applied-for example, after the removal of a literal or the replacement of a term-and since the dominant practice is to demodulate only after an inference rule has been completely applied, the proposed research focuses on an intriguing alternative. 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 Eneregy Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

The problem of choosing between using and avoiding equality predicates

This article is the twentieth of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks one to find criteria for effectively choosing between using and avoiding equality predicates. Since there exist inference rules (such as paramodulation) that enable an automated reasoning program to treat equality as understood, the discovery of such criteria would mark an important advance for the field. For evaluating a proposed solution to this research problem, we suggest possible test problems from group theory, ring theory, and Boolean algebra.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 automated theorem finding

This article is the twenty-fifth of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks one to identify appropriate properties to permit an automated reasoning program tofind new and interesting theorems, in contrast toproving conjectured theorems. Such programs are now functioning in many domains as valuable reasoning assistants. A sharp increase in their value would occur if they could also be used as colleagues to (so to speak) produce research on their own.This work was supported by the Office of Scientific Computing, 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 hyperparamodulation and nuclei

This article is the thirty-third of a series of articles discussing various open research problems in automated reasoning. The problem for research asks one to establish criteria for allowing certain — but not all — new clauses to become nuclei when using the inference rule hyperparamodulation or hyperresolution.This work was supported by the Office of Scientific Computing, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

基于证据推理的确定因子规则库推理方法

不确定性推理方法是人工智能领域的一个主要研究内容,If-then规则是人工智能领域最常见的知识表示方法. 文章针对实际问题往往具有不确定性的特点,提出基于证据推理的确定因子规则库推理方法.首先在If-then规则的基础上给出确定因子结构和确定因子规则库知识表示方法,该方法可以有效利用各种类型的不确定性信息,充分考虑了前提、结论以及规则本身的多种不确定性. 然后,提出了基于证据推理的确定因子规则库推理方法. 该方法通过将已知事实与规则前提进行匹配,推断结论并得到已知事实条件下的前提确定因子;进一步,根据证据推理算法得到结论的确定因子. 文章最后,通过基于证据推理的确定因子规则库推理方法在UCI数据集分类问题的应用算例,说明该方法的可行性和高效性.     

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 demodulating across argument and literal boundaries

This article is the twenty-fourth of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks one to find an appropriate theory for modulating across argument and across literal boundaries. Because demodulation has proved so useful—is most cases, even crucial—to automated reasoning, extending this concept to permit canonicalization to be applied at the predicate and at the clause and subclause levels merits exploration. For evaluating a proposed solution to this research problem, we suggest problems from mathematics, logic, program verification, database inquiry, 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-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 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.     

The problem of reasoning by analogy

This article is the twenty-seventh of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks one to find criteria that an automated reasoning program can apply to determine whether to attack a given question with reasoning by analogy. The imprecise term reasoning by analogy refers to a type of reasoning in which the type of proof being sought is sharply influenced by the style of proof that was successfully used to prove related theorems.This work was supported by the Office of Scientific Computing, 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.