Abstract
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.
Recommended Citation
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
Department(s)
Computer Science
International Standard Book Number (ISBN)
978-089791502-1
Document Type
Article - Conference proceedings
Document Version
Citation
File Type
text
Language(s)
English
Rights
© 2023 Association for Computing Machinery, All rights reserved.
Publication Date
01 Jan 1992
