Two Resolution Proof Strategies Developed by Peterson 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.
C. J. Merz and R. W. Wilkerson, "Experimentation with Proof Methods for Non-Horn Sets," Applied Computing: Technological Challenges of the 1990's, pp. 530 - 535, Association for Computing Machinery, Jan 1992.
The definitive version is available at https://doi.org/10.1145/143559.143683
International Standard Book Number (ISBN)
Article - Conference proceedings
© 2023 Association for Computing Machinery, All rights reserved.
01 Jan 1992