A DECISION PROCEDURE BASED ON THE RESOLUTION METHOD,
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. Friedman's decision procedure and on J. A. Robinson's 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)
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 01, 1968
- Accession Number
- AD0671994
Entities
People
- Bruce Kallick
Organizations
- Northwestern University