Accession Number:

AD0671994

Title:

A DECISION PROCEDURE BASED ON THE RESOLUTION METHOD,

Descriptive Note:

Corporate Author:

NORTHWESTERN UNIV EVANSTON ILL

Personal Author(s):

Report Date:

1968-07-01

Pagination or Media Count:

16.0

Abstract:

A decision procedure for satisfiability of predicate calculus formulas in the AAE prefix class is described. The procedure is a hybrid based on J. Friedmans decision procedure and on J. A. Robinsons resolution method. It most resembles the latter parent, in that resolvent clauses are formed from the clauses of a formula expressed in conjunctive normal form and from other resolvent clauses until two complementary one-literal clauses resolve into the empty clause. Unlike the general resolution method, however, the procedure does not generate literals with nested Skolem functions. There is, therefore, a bound on literal length and the procedure terminates even if the empty clause is not generated. Author

Subject Categories:

  • Theoretical Mathematics
  • Operations Research

Distribution Statement:

APPROVED FOR PUBLIC RELEASE