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):

Report Date:

1968-12-01

Pagination or Media Count:

19.0

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

Subject Categories:

  • Cybernetics

Distribution Statement:

APPROVED FOR PUBLIC RELEASE