Deleting Repeated Goals in the Problem Reduction Format
Donald W. Loveland, C. R. Reddy · Journal of the ACM · 1981
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 nontnvml