Extension Methods in Automated Deduction

Abstract

Calculi of first-order logic were developed for many different purposes, e.g., for (i) reconstructing mathematical proofs in a formal framework or (ii) for automated proof search. The old and “traditional” calculi, like Hilbert-type and Gentzen-type calculi, belong to the first category. Either they serve as a framework to a theory of provability, where not actual proofs but only their existence is of relevance, or they are used as instruments for proof transformations (e.g., cut-elimination in the sequent calculus). Specific rules like cut and modus ponens serve as proof building tools, which allow to combine lemmata to more complex proofs. The substitution rule (or elimination rule for quantifiers) is mostly formulated as a unary rule which can be applied independently of others. As the discipline of automated theorem proving evolved in the early sixties, the cut-rule and the unrestricted substitution rule were clearly defective features in a discipline of proof search. The first attempts to use Herbrand’s theorem directly and to reduce a first-order formula to a propositional one failed because of tremendous complexity. The paper of J. A. Robinson on the resolution principle (Robinson, 1965) then brought the decisive breakthrough: resolution was the first first-order calculus with a binary and minimal substitution principle — the well-known unification principle. Moreover, it works on quantifier-free conjunctive normal forms (clausal forms) which are logic-free (clauses can be represented as sequents of atoms). Resolution uses an atomic cut-rule in combination with the unification principle which allows for most general substitutions only. Thus, the key feature of resolution is minimality. Due to this minimality there are only finitely many deductions within a fixed depth, a property we call local finiteness. The price paid for this minimality is a loss of structure and an increase of proof complexity. The high proof complexity of computational calculi (like resolution, tableau calculi and connection calculi) forms a serious barrier to proof search for more complex theorems. The question arises, whether it is possible to combine the strong structural potential of the traditional logic calculi with the economical search features of computational calculi. To this aim, it is necessary to give up the strict minimality of the computational calculus without, at the same time, allowing the creation of arbitrary structures, signatures or lemmata. It is the purpose of this chapter to give a survey of different methods for introducing and preserving structure in automated deduction. The inference methods we present are extension methods in the sense that either the syntax is extended by predicate or function symbols or formulae are introduced which do not fulfill the (strict) subformula property. But all the rules we present here are computational in the sense that they are locally finite.