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 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 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 extending the set of support strategy

This article is the third of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research focuses on redefining or extending the definition of the set of support strategy so that the resulting strategy is as effective at all clause levels as it is at level 1. We include specific test problems for evaluating a proposed solution to this research problem.     

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 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 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 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 induction

This article is the thirtieth of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks for criteria for accurately determining when an induction argument is the appropriate form of argument for an automated reasoning program to employ. This research problem also asks for criteria for choosing well the property on which to conduct the induction argument.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.     

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 reasoning by case analysis

This article is the twenty-ninth 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 decide when to conduct a case analysis argument and to decide which cases are appropriate. When the choice of employing a case analysis argument is wise and the cases are well chosen, the likelihood that the reasoning program — or, for that matter, a person — will find an answer to the given question is sharply increased.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 reasoning from inequalities

This article is the twenty-first of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks one to find an inference rule that performs as paramodulation does, but with the focus on inequalities rather than on equalities. Since, too often, inequalities that are present in the input play a passive role during a reasoning program's attempt to complete an assignment, such an inference rule would markedly add to program effectiveness by giving inequalities the potential of playing a key role. For evaluating a proposed solution to this research problem, we suggest as possible test problems theorems from group theory and theorems from ring theory. This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract W-13-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 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 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 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 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 determining the size of a complete set of reductions

This article is the tenth of a series of articles discussing various open research problems in automated reasoning. Here we focus on finding criteria for accurately predicting the size of a complete set of reductions when such a set exists. 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.