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