Uniform proofs are sequent calculus proofs with the following characteristic: the last step in the derivation of a complex formula at any stage in the proof is always the introduction of the top-level logical symbol ofthat formula. We investigate the relevance of this uniform proof notion to structuring proof search in classical logic. A logical language in whose context provability is equivalent to uniform provability admits of a goal-directed proof procedure that interprets logical symbols as search directives whose meanings are given by the corresponding inference rules. While this uniform provability property does not hold directly of classical logic, we show that it holds of a fragment of it that only excludes essentially positive occurrences of universal quantifiers under a modest, sound, modification to the set of assumptions: the addition to them of the negation of the formula being proved. We further note that all uses of the added formula can be factored into certain derived rules. The resulting proof system and the uniform provability property that holds of it are used to outline a proof procedure for classical logic. An interesting aspect of this proof procedure is that it incorporates within it previously proposed mechanisms for dealing with disjunctive information in assumptions and for handling hypotheticals. Our analysis sheds light on the relationship between these mechanisms and the notion of uniform proofs.
Bibliographical noteFunding Information:
This work has grown out of a prior collaboration with Donald Loveland [6, 14] and has been enriched by his suggestions. We are also grateful to Robert Stark whose comments helped us discover an error in an earlier version of this paper. This work was started when the author was visiting Ludwig-Maximilians-UniversitatMunchen. Support from the Konrad Zuse-Programm administered by the Deutsche Akademischer Austauschdienst during this visit and subsequently from NSF Grant CCR-92-08465 is gratefully acknowledged.
- Classical logic
- Logic programming
- Proof search
- Proof theory
- Uniform provability