Accession Number : AD0671994

Title :   A DECISION PROCEDURE BASED ON THE RESOLUTION METHOD,

Corporate Author : NORTHWESTERN UNIV EVANSTON ILL

Personal Author(s) : Kallick,Bruce

Report Date : JUL 1968

Pagination or Media Count : 16

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)

Descriptors :   (*MATHEMATICAL LOGIC, ALGORITHMS), PROBLEM SOLVING, SET THEORY, DECISION THEORY, MATHEMATICAL MODELS, COMPUTER PROGRAMMING, THEOREMS

Subject Categories : Theoretical Mathematics
      Operations Research

Distribution Statement : APPROVED FOR PUBLIC RELEASE