Accession Number : AD0681170

Title :   A LINEAR FORMAT FOR RESOLUTION.

Descriptive Note : Interim rept.,

Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

Personal Author(s) : Loveland, D. W.

Report Date : DEC 1968

Pagination or Media Count : 19

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)

Descriptors :   (*COMPUTER LOGIC, RESOLUTION), SET THEORY, TOPOLOGY, THEOREMS.

Subject Categories : Cybernetics

Distribution Statement : APPROVED FOR PUBLIC RELEASE