An automatic theorem prover for substitution and detachment systems.
Jeremy George Peterson · Notre Dame Journal of Formal Logic · 1978
As mentioned in [3], the proofs exhibited in that paper were found with the aid of a theorem-proving computer program.This paper is a short summary of the algorithms and heuristics used.By a substitution and detachment system we mean any formal system whose language contains denumerably many variables and a finite set of connectives, including a distinguished binary connective which we callC.The theorems are the well-formed formulae which may be derived from a given set of well-formed formulae, called the axioms, by the rules of modus ponens (with respect to C) and substitution.We will assume all formulae to be in Polish prefix notation.It is known (cf.[7], p. 4) that Meredith's condensed detachment operator D provides an efficient method of presenting the proof of a theorem in such a system, but it does more than this.The result of applying modus ponens (with some appropriate substitutions) to the formulae Caβ and γ may be an infinite set of substitution instances of β.Some restriction must be placed on this set if modus ponens is to be mechanised.In using condensed detachment we choose the one member of this set, namely DCaβ.γ, which is most general in the sense that every other member of the set is a substitution instance of it [7], p. 4, as our result.J. Kalman has proved that every theorem which can be derived by modus ponens and substitution from a set of axioms is a substitution instance of a theorem which may be derived by condensed detachment alone.Thus we may use a theorem prover whose only rule of inference is condensed detachment to prove any theorem in a substitution and detachment system, if we consider that at each step not only the theorem derived but also all substitution instances of it have been proved.In practice it is rarely necessary to consider the substitution instances since theorems are usually required in the strongest possible form.That we can construct such a theorem prover follows from the fact that an algorithm is known for condensed detachment [l].