Accession Number : AD0674004

Title :   PROOF PROCEDURES AND DECISION PROCEDURES BASED ON THE RESOLUTION METHOD.

Descriptive Note : Doctoral thesis,

Corporate Author : NORTHWESTERN UNIV EVANSTON ILL DEPT OF INDUSTRIAL ENGINEERING AND MANAGEMENT SCIENCES

Personal Author(s) : Kallick,Bruce

Report Date : AUG 1968

Pagination or Media Count : 120

Abstract : A decision procedure for satisfiability of predicate calculus formulas in the E sub m A sub 2 E sub n prefix class is described. The procedure is a hybrid based on Joyce 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. Several examples are given and the procedure is compared with the two parent procedures. It is suggested that there may be some implications for theorem-proving procedures based on the resolution method in the direction of curtailing literal-length at the expense of increasing the required number of resolvents if in so doing the over-all computational effort can be reduced, e.g., by avoiding character manipulation. It is shown that the procedure may be readily modified to decide the two matrix-defined classes of Skolem normal form formulas whose solvability was established by Friedman's method. The procedure has been programmed (in Algol) for the restricted class of formulas having only dyadic predicates and some refutations produced by the program are included in an appendix. (Author)

Descriptors :   (*MATHEMATICAL LOGIC, PROBLEM SOLVING), DECISION THEORY, COMPUTER PROGRAMS, ALGORITHMS, THESES

Subject Categories : Theoretical Mathematics
      Operations Research

Distribution Statement : APPROVED FOR PUBLIC RELEASE