Abstract

Two resolution proof strategies developed by Peterson [ Pe76j are implemented by modifying Otter, an existing automated theorem prover. The methods, Lock-T refutation and LNL-T refutation, are generalizations of unit refutation and input refutation, respectively, to non-Hom sets and represent independent, equivalent but opposite ways of searching. Thus, the two techniques can be run simultaneously, exchanging only important intermediate results known as lemmas.

The algorithms used in the implementation, which are based on a corrected version of the foundational work, are outlined in detail and justified. Next, the newly implemented strategies are tested individually and together on various non-Horn challenge problems from the Tarskian Geometry and the Non-obvious problem. and these results are comparet.l with existing results on the same problems using other resolution techniques in Otter. It is shown that each method individually demonstrates the ability to efficiently construct proofs, and that in some cases running the two methods simultaneously is more efficient than running either method alone.

Department(s)

Computer Science

Comments

The first Author is a Graduate Student.

This report is substantially the M.S. thesis of the first author, completed May, 1991.

Report Number

CSc-91-05

Document Type

Technical Report

Document Version

Final Version

File Type

text

Language(s)

English

Rights

© 1991 University of Missouri - Rolla, All rights reserved

Publication Date

1991-05-01

Download

Share

 
COinS