
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 resolventclauses are formed from the clauses of a formula expressed in conjunctive normal form and from other resolventclauses until two complementary oneliteral clauses resolve into the empty clause. Unlike the general resolution method, however, the procedure does not generate literals with nested Skolemfunctions; there is therefore a bound on literallength 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 theoremproving procedures based on the resolution method in the direction of curtailing literallength at the expense of increasing the required number of resolvents if in so doing the overall 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 matrixdefined 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