Obvious Logical Inferences

OBVIOUS LOGICAL INFERENCES

1 Hartin Davis

Courant Institute of Mathematical Sciences, New York, U.S.A.

ABSTRACT

A precise definition is given of a class of inferences in predicate logic which it is proposed to identify with the class of "obvious" inferences. A mechanism for implementing "obvious inference" as a rule of inference in proof checking systems is discussed.

I. INTRODUCTION

Automatic proofchecking systems should be able to certify the correctness of any inference which users can see as obviously correct. It should only be necessary for a user to specify the premises and conclusion in calling for such certification. In proofchecking systems for predicate logic based on natural deduction, e.g. Stanford FOL [3], [6], [7], this facility is ordinarily available only for such special cases as tautological inference. The following example (taken from [5], p. 185) is instructive:

Although this inference seems a bit complicated at a first glance it is really obvious to anyone experienced with elementary logic. (The second and third premises provide an individual c for which Fe, Gc and (Yy)(Hcy · Ky) all hold. The first premise then gives an individual b such that Hcb and Jb. So Kb and Jb both must be true.) However a typical FOL proof would run to 17 lines. An "optimized" FOL proof using two calls to the TAUT tautological inference checker still runs 9 lines. A user is compelled to step-by-step eliminate quantifiers, use propositional calculus, and finally reinstate quantifiers.

In this communication, we will give a precise definition of a class of inferences in predicate logic we propose to identify with the classes of deductive inferences which, intuitively, are "obvious". We will describe a simple mechanism (based on a nonresolution Herbrand theorem-proving procedure) by means of which "obvious inference" can be implemented as a rule of inference in natural deduction systems, and we will describe All experimental. version of this mechanism as an extension of FOL. In particular the 9 to 17 steps required in the example cited is reduced to 1 when the new mec~dnism is available.

1 work supported by NSF Grant MCS 8Q-02438.

II. OBVIOUS HERBRAND PROOFS

What makes an inference obvious? Equivalently, what makes an inference complicated? We propose a~ an answer to the second question: an inference t~ complicated when it requires multiple substitutions from the Herbrand universe in the same clause. In such a case, a human being must exercise considerable ingenuity in order to find exactly the right substitutions from the typically infinite Herbrand universe. These considerations suggest the:

THESIS: An inference is obvious precisely when a Herbrand proof of its correctness can be given involving no more than one substitution instance of each clause.

Returning to our example, it is equivalent to the unsatisfiabiity of the list of clauses:

A Herbrand proof of the correctness of inference is obtained from the substitution: the

by checking that the resulting list of clauses is truth-functionally unsatisfiable. Indeed: there is only one substitution instance of each clause used, i~ accord with our thesis.

III. AUTOMATING OBVIOUS INFERENCE

How could this treatment of our example be automated? A first thought might be to use binary resolution with the restriction that no clause may be resolved upon more than once. But it is readily seen that an inauspicious order of resolutions can defeat this method. Thus, resolving (5) with (6) would give

Since the clauses (1), (2), (3), (4), (7), (8) are readily seen to be satisfiable, further use of resolution on these clauses alone cannot lead to a refutation. Of course, a resolution theorem-prover equipped with suitable heuristics could easily deal with this example. But it is not clear how to design an efficient resolution theorem-prover which will effectively verify all obvious inferences. Fortunately the method of linked conjuncts [1], [2) (which historically preceded resolution), can be used quite nicely for this purpose. The method is based on the simple remark that a set of clauses which is minimally truth-functionally unsatisfiable (in the sense that any proper subset is truth-functionally satisfiable) must be linked: that is, the negation of each literal occurring in one of the clauses must occur in one of the remaining clauses. Thus in order to test for obvious i-nferences one only need use the unification algorithm to search for all possible matches between literals and their negations using only.! single copy of each clause.

Our proposal is thus to adjoin to natural deduction proofcheckers a new rule of inference, OBVIOUS. OBVIOUS is invoked along with a list of premises and a proposed conclusion. (In the context of FOL, OBVIOUS has the same syntax as TAUT.) Invoking OBVIOUS calls an algorithm consisting of:

• (A) a preprocessor conclusion, Skolemizes and clauses; which negates the produces a list of
• (B) a procedure which searches the space of possible matches between literals and their negations;
• (C) a satisfiabiity tester (e.g. one based on the Davis-Putnam procedure [2], pp. 25-26).

If (A), (B), and (C) lead to success, i.e. to an unsatisfiable linked conjunct, the system adds the proposed conclusion as a new line in the proof being constructed. Otherwise, the system returns a message such as NOT OBVIOUS.

IV. EXPERIMENTS WITH FOL

During a brief stay at the Stanford AI Laboratory, the OBVIOUS rule was implemented along the lines discussed. A theorem-proving program based on the linked conjunct method that had been written by D. Mcilroy and Peter Hinman (see (1]) in 1962 was resurrected and modified. The nodification consisted of: (1) translation into the local dialect of LISP; (2) setting to 1 the parameters determining the maximum number of instances of each clause to be permitted; (3) placing a Skolemizing conjunctive normal form preprocessor at the front end of the program.

previously been the new OBVIOUS lengths of proofs approximately 10. dramatic reduction [4), which contains Various proofs that had checked by FOL were redone using facility. It was found that the were shortened by a factor of Opportunities for even more abound in Filman's dissertation over a thousand lines of FOL.

A version of OBVIOUS for general use with FOL will have to be modified to accommodate the rich FOL faciities for declaring variables to be of various "sorts". This can easily be done, either by modifying the unification algorithm subroutine in OBVIOUS to permit only substitutions of the correct sort, or by introducing into the preprocessor a preliminary procedure for making explicit the relativized quantifiers which the FOL sort mechanism suppresses.