Deduction Systems

The use of logic in the formalization of human reasoning can be traced back to the Greek philosophers, most notably Aristotle, whose primary concern was the investigation of the laws of human thought. With a collection of well-chosen axioms of logical deduction as a point of departure, Aristotle erected a theory of reasoning that endured nearly two thousand years before being developed further by such eminent logicians as Gottlob Frege (1848-1925), George Boole (1815-1864), and Bertrand Russell (1872-1970).

In this chapter we discuss the basic mathematical notions that we will need in the rest of this book. We expect that the concepts mentioned here are familiar to the reader, and so we do not provide a comprehensive treatment of them. Instead, our intent is to indicate briefly those ideas which will be used in later chapters, and to set the notation and terminology we will use in discussing them. For a more complete treatment of propositional and first-order logics, we recommend [Fit90], [Gal86], and [Men79]. Halmos’ treatment of introductory set theory ([Hal60]) is both elegant and accessible. Pure and algorithmic graph theory are the topics of [BM76] and [Gib85], respectively.

In this section the formal syntax of first-order logic is defined. As for any natural or artificial language, we require on the one hand an alphabet on which the language is based, and on the other a grammar according to which sentences in the language are constructed.

Formulae, it must be remembered, are nothing more than words over an alphabet. But logical formulae were originally developed as a means of describing properties of mathematical structures, and so a reasonable semantics of a first-order language would be one which interprets its formulae in a concrete mathematical structure.

One of the central concepts introduced in the previous chapter is the notion of semantic consequence and, as indicated, mathematical theorem development is based on this notion. Unfortunately, semantic consequence as defined there is not mechanizable, since it is not possible in general to investigate all of the—potentially infinitely many—models of a given set of formulae. In this chapter we introduce a notion of syntactic consequence and prove that it is equivalent to that of semantic consequence. The notion of syntactic consequence we will discuss corresponds to an efficiently mechanizable calculus, namely, the Gentzen calculus G of Gerhard Gentzen.

The Gentzen calculus introduced in the last chapter provides a relatively straightforward method for demonstrating validity of first-order formulae, and one whose completeness can be proved directly. But—practically speaking—Gentzen calculi suffer quite serious disadvantages, unfortunately rendering them unsuitable for use in mechanizing proofs without extensive modification. The primary obstacles to their efficient automation are the nondeterminism, at any given stage of proof development, of the choice of rule to be applied as well as of the formula to which to apply it, and the unguided consideration of all terms for substitution in applications of the quantifier rules. In a derivation it is possible, for example, that the quantifier rules can be applied repeatedly to the same formula to the exclusion of applications of other rules needed for the successful development of a proof, or that in applying a quantifier rule, the bound variables of the formula will never be instantiated by the “right” substitution terms. We will see in Theorems 6.2.1 and 6.3.2 that restricting the syntactic forms that formulae to be proved may have, and then showing that every formula can be converted to a semantically equivalent formula meeting these syntactic requirements, will allow us to correspondingly restrict the structure of proof trees for valid formulae. From such proof trees in “standard form” we may derive significantly simpler formulae provable iff the original formulae are. This “preprocessing” of formulae in the Gentzen calculus thus emerges as a basis for deriving quite effective calculi for automating deduction. In this book, Gentzen calculi will serve primarily as a point of departure for discussing one particular class of such calculi, namely, resolution calculi, and for discussing Herbrand’s Theorem, the foundation for proving the refutation completeness of such calculi.

Our results from Chapter 6 suggest that an arbitrary formula ϕ can be proved—and hence ¬ϕ can be refuted—by first converting ¬ϕ to a satisfiability-equivalent formula ψ in prenex normal form, and then refuting a set of instantiated clauses—derived from the clausal form of the matrix of F(ψ)—which is ground satisfiable over the extended Herbrand universe of ϕ iff ¬ϕ satisfiable. The existence of such a set of instantiated clauses is guaranteed by Herbrand’s Theorem, whose proof, unfortunately, provides no insight into how to actually find one. A rather straightforward method for generating a set of clauses with the required property is simply to enumerate, in turn, all ground instances of the clauses in the matrix of F(ψ) until such a set is found; in practice, however, this kind of uncontrolled enumeration emerges as considerably less than efficient. In the next section we will learn of unification, a technique for eliminating brute-force enumeration of ground clauses from our refutation method for arbitrary formulae by enabling the systematic recognition of ground instances of nonground clauses which are relevant to refutations. The remainder of this section is dedicated to describing a refutation method for ground clauses that can be used in conjunction with precisely such a brute-force enumeration; in Section 7.4 we see how to combine unification with a generalization of this method for ground clauses to arrive at an efficient refutation technique for arbitrary clauses.

Generalizing Theorem 7.4.3, we may infer that an arbitrary resolution calculus is refutation complete if, for every unsatisfiable set S of clauses and every fair derivation out of S, the empty clause lies in the resolution search space generated from S by that calculus. In particular, since fair derivation strategies provide means of traversing entire resolution search spaces, in proving the refutation completeness of a given resolution calculus it suffices to consider only completeness with respect to fair derivations. Completeness of the calculus in question then follows by demonstrating the existence of at least one fair derivation strategy for it.

With regard to improving the efficiency of automated deduction systems, the final word has not yet been spoken. In Chapter 8 we became acquainted with various techniques for pruning search spaces associated with deduction, most of which rely on restricting applications of the resolution and factorization rules. While such methods are indeed helpful in constructing more efficient resolution theorem provers, in fact some of the most promising techniques for increasing deduction efficiency have been based not on methods for restricting the application of deduction rules, but rather on modifications of the input calculi themselves. Two general tendencies in modifying calculi for efficiency are clearly discernible. The first is the development of special calculi for particular commonly occurring predicates. A classic example of this approach to improving deduction efficiency is the development of completion procedures—based on the Knuth-Bendix algorithm—for equational logic. The second tendency is that of using knowledge about special functions or predicates to arrive at more powerful unification algorithms. The fundamental idea behind this latter approach is to hand over the lion’s share of the deduction work to the (deterministic) unification mechanism, and so to reduce the computational burden placed on the (nondeterministic) logical inference system.