Deleting Repeated Goals in the Problem Reduction Format
- 1 October 1981
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 28 (4) , 646-661
- https://doi.org/10.1145/322276.322278
Abstract
Although the classical problem reducUon format for orgamzmg automauc proof search is incomplete, a complete extension of the format is known ElimmaUon of tdentlcal descendent subgoals is a well-known deletion rule for the classical format but is not obviously vahd m the extended format. Because of ~ts mtumve appeal and ease of apphcatlon, one would wish to know that the rule ~s safe to use m the extended format It ts shown here that the deleuon rule is indeed safe The result appears to be decidedly nontnvmlKeywords
This publication has 2 references indexed in Scilit:
- A man-machine theorem-proving systemArtificial Intelligence, 1974
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965