Experimentation with proof methods for non-Horn sets
Chris Merz, Ralph W. Wilkerson · 1992
Two resolution proof strategies developed by Peterson [4] 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 resolution, respectively, to non-Horn sets and represent independent, equivalent but opposite ways of searching.The algorithms used are based on a corrected version of the foundational work.The strategies have been tested on various non-Horn challenge problems from the Tarskian Geometry and the Non-Obvious problem, with the results being in some cases quite favorable when compared to other resolution techniques.