A LINEAR FORMAT FOR RESOLUTION.
CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
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