A LINEAR FORMAT FOR RESOLUTION.
Abstract
The Resolution procedure of J.A. Robinson is shown to remain a complete proof procedure when the refutations permitted are restricted so that clauses C and D and resolvent R of clauses C and D meet the following conditions: (1) C is the resolvent immediately preceding R in the refutation if any resolvent precedes R, (2) either D is a member of the given set S of clauses or D precedes C in the refutation and R subsumes an instance of C or R is the empty clause, and (3) R is not a tautology. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 01, 1968
- Accession Number
- AD0681170
Entities
People
- D. W. Loveland
Organizations
- Carnegie Mellon University