Some Linear Herbrand Proof Procedures: An Analysis,
Abstract
Several Herbrand proof procedures proposed during the 1960 decade are shown to be related in varying degrees. Most of the paper deals with a relationship between s-linear resolution and model elimination. Refinements of each are proposed and the spaces of ground deductions are shown to be isomorphic in a suitable sense. The two refined procedures are then studied at the general level where they are no longer isomorphic and do not always relate to a natural ground level counterpart. Other topics considered are the introduction of an added merge condition to model elimination and also an expanded possible use of lemmas. Finally, the model elimination procedure is interpreted in the linked conjunct procedure of Davis and the matrix reduction procedure of Prawitz. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 01, 1970
- Accession Number
- AD0717753
Entities
People
- D. W. Loveland
Organizations
- Carnegie Mellon University