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

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

Some obstacles to the automation of reasoning,and the problem of redundant information

This article is the first of a series of articles discussing various unsolved research problems in automated reasoning. We begin with an overview of some of the main obstacles that prevent reasoning programs from being even more useful than they currently are. We include a brief discussion of the basic paradigm used by those programs whose power is demonstrated by their use in answering open questions from mathematics. We then turn our attention to an unsolved research problem concerned with finding a strategy to avoid or reduce the deduction of redundant information.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 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 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 naming and function replacement

This article is the twenty-eighth 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 profitably use to remove functions present in the representation and replace them with appropriate predicates or constants thatname the entities that werenamed by the functions. The notation used to present a problem to a reasoning program can have a profound effect on the likelihood of the program's success.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 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 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 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 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.     

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.