Automation of Reasoning

In this article we give a critical history of automated theorem proving from 1965 through 1970. By evaluating the contributions of the period, we provide a guide to a study of the field during its development. In order to differentiate between that work which turned out to be significant and that which had lesser impact, we occasionally rely of necessity on developments occurring after 1970. Since we confine our attention to automated theorem proving, certain work in logic occurring in the period in question is ignored. For example, various studies on decidability and complexity are excluded from comment because they are not directly germane. In addition to providing a critique, we have the secondary objective of giving a tutorial. We provide sufficient information and definition to permit one to read this article with minimal recourse to the literature. In this regard we often replace the very rigorous treatment of a concept by a more intuitive description.

The purpose of the present essay is to set forth a convenient algorithm for the lower functional calculus with identity. The method is open-ended when applied to formulae of certain types and so, as was to be expected, it cannot in general be relied upon to show something not to be a logical truth when in fact it is not one. But when the method is applied to a formula expressing a logical truth, the method will eventually show it to be such, and it will not show something to be a logical truth unless it really is. The proof of these facts will not be given here, but it should be clear that the method is closely related to known systems with respect to which results of this sort have been established. These are the systems of natural deduction, either conceived syntactically2 or semantically3. Methods of this type have been adapted for use with electronic computers4. However, the cancellation algorithm presented here is primarily designed for use with computers4 made of pencil and paper, and its convenience is to be judged in those terms. It is a mechanical procedure which is designed to provide maximum opportunity for shortcuts based on simple insight; it stands to conventional methods rather as Quine’s truth-value analysis stands to the full truth-table method.

In [1, 2] we presented several aspects of the inverse method of establishing the deducibility of formulas of the classical predicate calculus. This method is profitable for constructing mechanical proof search algorithms, but a variant of a method described in [1] is applicable only for disjunctions of prenexed formulas whose matrices are in conjunctive normal form. In general putting a formula F in prenex form F’ and then finding a deduction of F’ involves more complex and cumbersome calculations than attacking F directly. Here the inverse method allows us to drop many of the superfluities in searching for proofs of arbitrary formulas. The purpose of this paper is to give a sketchy description of the inverse method of establishing the deducibility of arbritrary formulas of C’, the classical predicate calculus with function symbols.

The theory of J. A. Robinson’s resolution principle, an inference rule for first-order predicate calculus, is unified and extended. A theorem-proving computer program based on the new theory is proposed and the proposed semantic resolution program is compared with hyper-resolution and set-of-support resolution programs. Renamable and semantic resolution are defined and shown to be identical. Given a model M, semantic resolution is the resolution of a latent clash in which each “electron” is at least sometimes false under M; the nucleus is at least sometimes true under M.The completeness theorem for semantic resolution and all previous completeness theorems for resolution (including ordinary, hyper-, and set-of-support resolution) can be derived from a slightly more general form of the following theorem. If U is a finite, truth-functionally un-satisfiable set of nonempty clauses and if M is a ground model, then there exists an unresolved maximal semantic clashE ₁ , E ₂ , ..., E _q , C with nucleus C such that any set containing C and one or more of the electrons E₁, E₂, ..., Eq is an unresolved semantic clash in U.

In many fields of mathematics the richness of the underlying axiom set leads to the establishment of a number of very general equalities. For example, it is easy to prove that in groups (x -1)-1= x and that in rings -x•-y = x •y. In the presence of such an equality, each new inference made during a proof search by a theorem-proving program may immediately yield a set of very closely related inferences. If, for example, b •a = c is inferred in the presence of (x-1)-1= x, substitution immediately yields obviously related inferences such as (b-1)-1 • a = c. Retention of many members of each such set of inferences has seriously impeded the effectiveness of automatic theorem proving. Similar to the gain made by discarding instances of inferences already present is that made by discarding instances of repeated application of a given equality. The latter is achieved by use of demodulation. Its definition, evidence of its value, and a related rule of inference are given. In addition a number of concepts are defined the implementation of which reduces both the number and sensitivity to choice of parameters governing the theorem-proving procedures.

A refinement of the resolution method for mechanical theorem proving is presented. A resolvent C of clauses A and B is called a merge if literals from A and B merge together to form some literal of C. It is shown that the resolution method remains complete if it is required that two noninitial clauses which are not merges never be resolved with one another. It is also shown that this strategy can be combined with the set-of-support strategy.

In [3], [4], and [5] Joyce Friedman formulated and investigated certain rules which constitute a semi-decision procedure for wffs of first order predicate calculus in closed prenex normal form with prefixes of the form ∀x₁...∀x_k∃y₁...∃Ym∀z₁...∀z _n . Given such a wff QM,where Q is the prefix and M is the matrix in conjunctive normal form, Friedman’s rules can be used, in effect, to construct a matrix M* which is obtained from M by deleting certain conjuncts of M. Obviously, ⊢QM⊃QM* Using the Herbrand-Gödel theorem for first order predicate calculus, Friedman showed that ⊢QM if and only if ⊢QM*. Clearly if M* is the empty conjunct (i.e., a tautology), ⊢QM* so ⊢QM. Friedman also showed that for certain classes of wffs, such as those in which m ≤ 2 or n = 0 in the prefix above, ⊢QM if and only if M* is the empty conjunct. Hence for such classes of wffs the rules constitute a decision procedure. Computer implementation [4] of the procedure has shown it to be quite efficient by present standards.

A proof procedure based on a theorem of Herbrand and utilizing the matching technique of Prawitz is presented. In general, Herbrand-type proof procedures proceed by generating ever increasing numbers of candidates for the truth-functionally contradictory statement the procedures seek. A trial is successful when some candidate is in fact a contradictory statement. In procedures to date the number of candidates developed before a contradictory statement is found (if one is found) varies roughly exponentially with the size of the contradictory statement. (“Size” might be measured by the number of clauses in the conjunctive normal form of the contradictory statement.) Although basically subject to the same rate of growth, the procedure introduced here attempts to drastically trim the number of candidates at an intermediate level of development. This is done by retaining beyond a certain level only candidates already “partially contradictory.” The major task usually is finding the partially contradictory sets. However, the number of candidate sets required to find these subsets of the contradictory set is generally much smaller than the number required to find the full contradictory set.

The generalized resolution principle is a single inference principle which provides, by itself, a complete formulation of the quantifier-free first-order predicate calculus with equality. It is a natural generalization of the various versions and extensions of the resolution principle, each of which it includes as special cases; but in addition it supplies all of the inferential machinery which is needed in order to be able to treat the intended interpretation of the equality symbol as ‘built in’, and obviates the need to include special axioms of equality in the formulation of every theorem-proving problem which makes use of that notion.

The exclusive use of first-order logic in mechanical theorem proving systems effectively prevents the formulation of most interesting problems for input to them, while the use of higher-order logic would not. Yet if the higher-order notion of logical validity is construed, following Henkin. as “true under all interpretations, standard or not”, as is advocated here, then full omega-order logic still has a mechanical proof procedure. Furthermore, since Takeuti’s conjecture is now known to be correct, this procedure can be given the direct “semantic tableau” form. A version of this procedure is presented, based on SchUtte’s but exploiting Hilbert’s epsilon operator.

AUTOMATH is a language intended for expressing detailed mathematical thoughts. It is not a programming language, although it has several features in common with existing programming languages. It is defined by a grammar, and every text written according to its rules is claimed to correspond to correct mathematics. It can be used to express a large part (see 1.6) of mathematics, and admits many ways for laying the foundations. The rules are such that a computer can be instructed to check whether texts written in the language are correct. These texts are not restricted to proofs of single theorems; they can contain entire mathematical theories, including the rules of inference used in such theories.

The fifth in a series of experiments in semi-automated mathematics is described. These experiments culminated in large complex computer programs which allow a mathematician to prove mathematical theorems on a man/machine basis. SAM V, the fifth program, is oriented primarily toward the development of efficient automatic techniques for handling some of the more basic processes of mathematical deduction, and toward the realization of efficient real-time interaction between man and machine through the use of cathode-ray tube displays. SAM V’s most notable success is the solution of an open problem in lattice theory.

We investigate in this paper the application of a modified version of semantic trees (Robinson 1968) to the problem of finding efficient rules of proof for mechanical theorem-proving. It is not our purpose to develop the general theory of these trees. We concentrate instead on those cases of semantic tree construction where we have found improvements of existing proof strategies. The paper is virtually self-contained and to the extent that it is not, Robinson’s review paper (1967) contains a clear exposition of the necessary preliminaries.

An alternate approach to the formulation of the Model Elimination proof pro­cedure is presented. By exploiting fully the ability to linearize the procedure format (isolating the format from a tree structure form) and by representing lemmas by clauses, the description of the Model Elimination procedure is greatly simplified.

A new format for the Model Elimination procedure simpler in structure than the original is presented here. In this form the Model Elimination procedure exhibits a compatibility with the Resolution procedure. Two ways in which this compatibility can be used to design improved theorem-provers are considered, including a strategy designed for problems too complex to be completely solved before memory is filled using either of the procedures mentioned above.

Of the theorem-proving (deducibility-establishing) methods used in recent years with orientation toward the synthesis of machine algorithms and programs, the resolution method proposed in 1964 by J. A. Robinson [1,2] has gained the greatest reputation and enjoyed the most theoretical development. Concurrently and independently, the present author proposed the so-called “inverse method”, which is also designed for the automation of theorem proving [3,4,5]. The domain of applicability of the inverse method is wider, but in application to the same calculus (the classical predicate calculus with function symbols) and to the same standardization of the initial formulas as the resolution method it is very convenient to compare and interfuse the two methods. The purpose of the present article is to establish a relationship between the methods whereby it will be possible to transfer the results obtained by one method to the other (we are thinking by and large in terms of results bearing on the completeness of particular deducibility-establishing tactics).

The E-Resolution inference principle described in this paper is a single-inference logic system for the first-order predicate calculus with equality. Special axioms for equality (i.e., axioms for symmetry, reflexivity, transitivity, and substitutivity) are not required to be added to the original set of clauses. Other advantages of E-Resolution are the relatively small number of intermediate clauses which must be retained in a proof and the distinct possibility that search strategies suitable for Resolution will also be suitable for E-Resolution. Although it is not known whether or not E-Resolution is complete, this topic is currently being investigated by the author.

In this paper, I first give a simplified description of the method proposed in my earlier paper ‘An improved proof procedure’. This method is then further developed in order to diminish the work of finding a substitution that makes a given formula inconsistent. Finally, the possibility of developing the method in another direction is discussed.By a proof procedure (or proof method) I understand in this connection an algorithm A with the property: for any valid formula F in the predicate calculus, A(F) (i.e., the result of applying A to F) is a proof of F. Equivalently, one may consider algorithms A with the property: if F is not satisfiable, then A(F) is a refutation of F. Following a tradition, I shall use this latter formulation. (It is of course immaterial which formulation one chooses, and when it comes to programming the procedure, all differences disappear completely.)

A term is an individual constant or variable or an n-adic function letter followed by n terms. An atomic formula is an n-adic predicate letter followed by n terms. A literal is an atomic formula or the negation thereof. A clause is a set of literals and is thought of as representing the universally-quantified disjunction of its members. It will sometimes be notationally convenient1 to distinguish between the empty clause □, viewed as a clause, and ‘other’ empty sets such as the empty set of clauses, even though all these empty sets are the same set-theoretic object ø. A ground clause (term, literal) is one with no variables. A clause C’ (literal, term) is an instance of another clause C (literal, term) if there is a uniform replacement of the variables in C by terms that transform C into C’.

Since their introduction in 1965,7 resolution based deductive systems for the first-order predicate calculus have been extensively investigated and utilized by researchers in the field of automatic theorem-proving by computer. Part of this research has been directed at finding techniques for treating the equality relation within the framework of resolution based deductive systems.2,3,4,5,9,10 Perhaps the most natural treatment of equality, introduced so far, is by means of the para-modulation principle which when used in conjunction with resolution forms a complete deductive system for the first-order predicate calculus with equality.5,6,11A very similar technique for treating equality was introduced4 and called E-resolution. In fact E-resolution can be viewed as a restricted form of paramodulation and resolution. The purpose of this paper is to define E-resolution in terms-of paramodulation and resolution and to prove the completeness of E-resolution and several modifications of E-resolution.

A new technique is given for establishing the completeness of resolution-based deductive systems for first-order logic (with or without equality) and several new completeness results are proved using this technique. The technique leads to very simple and clear completeness proofs and can be used to establish the completeness of most resolution-based deductive systems reported in the literature. The main new result obtained by means of this technique is that a linear format for resolution with merging and set of support and with several further restrictions is a complete deductive system for the first-order predicate calculus.

A resolution in which one of the two parent clauses is a unit clause is called a unit resolution, whereas a resolution in which one of the two parent clauses is an original input clause is called an input resolution. A unit (input) proof is a deduction of the empty clause q such that every resolution in the deduction is a unit (input) resolution. It is proved in the paper that a set S of clauses containing its unit factors has a unit proof if and only if S has an input proof. A LISP program implementing unit resolution is described and results of experiments are given.

An algorithm is described which is capable of solving certain word problems: i.e. of deciding whether or not two words composed of variables and operators can be proved equal as a consequence of a given set of identities satisfied by the operators. Although the general word problem is well known to be unsolvable, this algorithm provides results in many interesting cases. For example in elementary group theory if we are given the binary operator ·, the unary operator −, and the nullary operator e, the algorithm is capable of deducing from the three identities a · (b · c) = (a · b) · c, a · a− = e, a · e = a, the laws a− · a = e, e · a = a, a− − = a, etc.; and furthermore it can show that a · b = b · a− is not a consequence of the given axioms.The method is based on a well-ordering of the set of all words, such that each identity can be construed as a “reduction”, in the sense that the right-hand side of the identity represents a word smaller in the ordering than the left-hand side. A set of reduction identities is said to be “complete” when two words are equal as a consequence of the identities if and only if they reduce to the same word by a series of reductions. The method used in this algorithm is essentially to test whether a given set of identities is complete; if it is not complete the algorithm in many cases finds a new consequence of the identities which can be added to the list. The process is repeated until either a complete set is achieved or until an anomalous situation occurs which cannot at present be handled.Results of several computational experiments using the algorithm are given.

The use of equality axioms in resolution refutation systems has seemed to be particularly inefficient. In order to remedy this difficulty several modifications of the resolution method have been proposed ([4], [13], [15], [17] and [21] and more recently [2] and [10]). Of these the paramodulation strategy of [15] seems to be particularly simple and efficient. The method for dealing with equality investigated in this paper consists of using equality axioms and of applying the version of hyper-resolution proposed in [5]. The hyper-resolution and para-modulation methods are compared and a simple interpretation of the former is found in a subsystem of the latter, providing a straightforward proof for the completeness of this subsystem of paramodulation. Several proposals are put forward for modifying the hyper-resolution method and these modifications are seen to induce corresponding modifications of the paramodulation strategy.

The Resolution procedure of J. A. Robinson is shown to remain a complete proof procedure when the refutations permitted are restricted so that clauses C and D and resolvent R of clauses C and D meet the following conditions: (1) C is the resolvent immediately preceding R in the refutation if any resolvent precedes R, (2) either D is a member of the given set S of clauses or D precedes C in the refutation and R subsumes an instance of C or R is the empty clause, and (3) R is not a tautology.

We present an outline of the principal features of an on-line interactive theorem-proving program, and a brief account of the results of some experiments with it. This program has been used to obtain proofs of new mathematical results recently announced without proof in the Notices of the American Mathematical Society.

The paper discusses some basic refinements of the Resolution Principle which are intended to improve the speed and efficiency of theorem-proving programs based on this rule of inference. It is proved that two of the refinements preserve the logical complete­ness of the proof procedure when used separately, but not when used in conjunction. The results of some preliminary experiments with the refinements are given.

The question of the minimum complexity of derivation of a given formula in classical propositional calculus is considered in this article and it is proved that estimates of complexity may vary considerably among the various forms of propositional calculus. The forms of propositional calculus used in the present article are somewhat unusual, † but the results obtained for them can, in principle, be extended to the usual forms of propositional calculus.

In [8] J. A. Robinson introduced a complete refutation pro­cedure called resolution for first order predicate calculus. Resolution is based on ideas in Herbrand’s Theorem, and provides a very convenient framework in which to search for a proof of a wff believed to be a theorem. Moreover, it has proved possible to formulate many refinements of resolution which are still complete but are more efficient, at least in many contexts. However, when efficiency is a prime consideration, the restriction to first order logic is unfortunate, since many state­ments of mathematics (and other disciplines) can be expressed more simply and naturally in higher order logic than in first order logic. Also, the fact that in higher order logic (as in many-sorted first order logic) there is an explicit syntactic distinc­tion between expressions which denote different types of intuitive objects is of great value where matching is involved, since one is automatically prevented from trying to make certain inappropriate matches. (One may contrast this with the situation in which mathematical statements are expressed in the symbolism of axiomatic set theory.)

A theorem proving program has been written in LISP which attempts to speed up automatic theorem proving by the use of heuristics. Some of these heuristics are of a general nature, applicable to the proof of any theorem in mathematics, while others are designed for set theory. Their effect is to break the theorem into parts which are easier to prove. The proof of these parts is then attempted by resolution. Resolution, when used, is relegated to the job it does best, proving relatively easy assertions.This program has been used to prove a large number of theorems in set theory, many of which would be impossible (because of time and storage restrictions) by current resolution methods.

The object of the present article is to give a brief description of an algorithm developed by the Mathematical Logic Group of the Leningrad Branch of the V.A. Steklov Mathematical Institute (LOMI) of the Academy of Sciences of the USSR for the determination of deducibility in the classical predicate calculus with function symbols. The deducibility determination algorithm (DDA) has its theoretical foundation in the inverse method of establishing deducibility for logical calculi, as described, for example, in [1]; we shall use the terminology of the latter without further explanations.

Linear resolution with selection function (SL-resolution) is a restricted form of linear resolution. The main restriction is effected by a selection function which chooses from each clause a single literal to be resolved upon in that clause. This and other restrictions are adapted to linear resolution from Loveland’s model elimination.We show that SL-resolution achieves a substantial reduction in the generation of redundant and irrelevant derivations and does so without significantly increasing the complexity of simplest proofs. We base our argument for the increased efficiency of SL-resolution upon precise calculation of these quantities.A more far reaching advantage of SL-resolution is its suitability for heuristic search. In particular, classification trees, subgoals, lemmas, and and/or search trees can all be used to increase the efficiency of finding refutations. These considerations alone suggest the superiority of SL-resolution to theorem proving procedures constructed solely for their heuristic attraction.From comparison with other theorem proving methods, we conjecture that best proof procedures for first order logic will be obtained by further elaboration of SL-resolution.

In recent years the idea of using electronic computers to search for proofs of theorems of quantification theory has drawn considerable attention. One of the more successful methods of attack on the problem has stemmed from the work of Quine [12], Gilmore [5], Davis and Putnam [4] and J. Alan Robinson [16]. This paper is concerned with a portion of the theory underlying an extension of this line of development to systems — first-order theories with equality — in which there is a distinguished relation symbol for equality. The field of mathematics upon which we have concentrated our computer experiments in order to study various properties of our procedure is first-order group theory.