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
Descriptors:
Subject Categories:
- Theoretical Mathematics
- Operations Research