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 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 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 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 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 power of combining resonance with heat

In this article, I present experimental evidence of the value of combining two strategies each of which has proved powerful in various contexts. The resonance strategy gives preference (for directing a program's reasoning) to equations or formulas that have the same shape (ignoring variables) as one of the patterns supplied by the researcher to be used as a resonator. The hot list strategy rearranges the order in which conclusions are drawn, the rearranging caused by immediately visiting and, depending on the value of the heat parameter, even immediately revisiting a set of input statements chosen by the researcher; the chosen statements are used to complete applications of inference rules rather than to initiate them. Combining these two strategies often enables an automated reasoning program to attack deep questions and hard problems with far more effectiveness than using either alone. The use of this combination in the context of cursory proof checking produced most unexpected and satisfying results, as I show here. I present the material (including commentary) in the spirit of excerpts from an experimenter's notebook, thus meeting the frequent request to illustrate how a researcher can make wise choices from among the numerous options offered by McCune's automated reasoning program OTTER. I include challenges and topics for research and, to aid the researcher, in the Appendix a sample input file and a number of intriguing proofs.This work was supported by the Mathematical, Information, and Computational Sciences Division subprogram of the Office of Computational and Technology 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.     

Discovering inequality conditions in the analytic solution of optimization problems

Necessary and sufficient conditions for the problem of maximizing or minimizing a function subject to inequality constraints are given by a set of equalities and inequalities known as the Kuhn-Tucker conditions. These conditions can provide an analytic solution to the optimization problem if the artificial variables known as Lagrange multipliers can be eliminated. However, this is tedious to do by hand. This paper develops a computer program to assist in the solution process which combines symbolic computation and automated reasoning techniques. The program may also be useful for other problems involving algebraic reasoning with inequalities which employ general functions or symbolic parameters.     

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

Solving open problems in right alternative rings with Z-module reasoning

This paper presents our experiments using an automated reasoning program, called the Z-module reasoning system, to prove a number of interesting theorems in right alternative rings. Important results include a computer solution of the conjecture that (x, x, y)² x(x, x, y) ²=0 holds in every right alternative ring and a computer solution of a generalized version of this conjecture. The paper illustrates how one uses the Z-module reasoning system to solve different problems with varying complexity.This research 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 Shortest 2-Basis for Boolean Algebra in Terms of the Sheffer Stroke

In this article, we present a short 2-basis for Boolean algebra in terms of the Sheffer stroke and prove that no such 2-basis can be shorter. We also prove that the new 2-basis is unique (for its length) up to applications of commutativity. Our proof of the 2-basis was found by using the method of proof sketches and relied on the use of an automated reasoning program. This revised version was published online in August 2006 with corrections to the Cover Date.     

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 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 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 kernel strategy and its use for the study of combinatory logic

Barendregt defines combinatory logic as an equational system satisfying the combinatorsS andK with ((Sx)y)z=(xz)(yz) and (Kx)y=x; the set consisting ofS andK provides abasis for all of combinatory logic. Rather than studying all of the logic, logicians often focus onfragments of the logic, subsets whose basis is obtained by replacingS orK or both by other combinators. In this article, we present a powerful new strategy, called thekernel strategy, for studying fragments in the context of questions concerned with fixed point properties. Interest in such properties rests in part with their relation to normal forms and paradoxes. We show how the kernel strategy was used to answer a number of open questions, offering abundant evidence that the availability of the kernel strategy marks a singular advance for automated reasoning. In all of our experiments with this strategy applied by an automated reasoning program, the rate of success has been impressively high and the CPU time to obtain the desired information startlingly small. For each fragment we study, we use the kernel strategy to attempt to determine whether the strong or the weak fixed point property holds. WhereA is a given fragment with basisB, the strong fixed point property holds forA if and only if there exists a combinatory such that, for all combinatorsx,yx=x(yx), wherey is expressed purely in terms of elements ofB. The weak fixed point property holds forA if and only if for all combinatorsx there exists a combinatory such thaty=xy, wherey is expressed purely in terms of the elements ofB and the combinatorx. Because the use of the kernel strategy is so effective in addressing questions focusing on either fixed point property, its formulation marks an important advance for combinatory logic. Perhaps of especial interest to logicians is an infinite class of infinite sets of tightly coupled fixed point combinators (presented here), whose unexpected discovery resulted directly from the application of the strategy by an automated reasoning program. We also offer various open questions for possible research and focus on an automated reasoning program and input files that may prove useful for such research.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 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.     

Robbins algebra: Conditions that make a near-boolean algebra boolean

Some problems posed years ago remain challenging today. In particular, the Robbins problem, which is still open and which is the focus of attention in this paper, offers interesting challenges for attack with the assistance of an automated reasoning program; for the study presented here, we used the program OTTER. For example, when one submits this problem, which asks for a proof that every Robbins algebra is a Boolean algebra, a large number of deduced clauses results. One must, therefore, consider the possibility that there exists a Robbins algebra that is not Boolean; such an algebra would have to be infinite. One can instead search for properties that, if adjoined to those of a Robbins algebra, guarantee that the algebra is Boolean. Here we present a number of such properties, and we show how an automated reasoning program was used to obtain the corresponding proofs. Additional properties have been identified, and we include here examples of using such a program to check that the corresponding hand-proofs are correct. We present the appropriate input for many of the examples and also include the resulting proofs in clause notation.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.     

Automatic symbolic compositional verification by learning assumptions

Compositional reasoning aims to improve scalability of verification tools by reducing the original verification task into subproblems. The simplification is typically based on assume-guarantee reasoning principles, and requires user guidance to identify appropriate assumptions for components. In this paper, we propose a fully automated approach to compositional reasoning that consists of automated decomposition using a hypergraph partitioning algorithm for balanced clustering of variables, and discovering assumptions using the L ^* algorithm for active learning of regular languages. We present a symbolic implementation of the learning algorithm, and incorporate it in the model checker NuSmv. In some cases, our experiments demonstrate significant savings in the computational requirements of symbolic model checking. This research was partially supported by ARO grant DAAD19-01-1-0473, and NSF grants ITR/SY 0121431 and CCR0306382.     

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.