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

This paper concerns both the complexity aspects of PA and the pragmatics of improving algorithms for dealing with restricted subcases of PA for uses such as program verification. We improve the Cooper-Presburger decision procedure and show that the improved version permits us to obtain time and space upper bounds for PA classes restricted to a bounded number of alternations of quantifiers. The improvement is one exponent less than the upper bounds for the decision problem for full PA. The pragmatists not interested in complexity bounds can read the results as substantiation of the intuitive feeling that the improvement to the Cooper-Presburger algorithm is a real, rather than ineffectual, improvement. (It can be easily shown that the bounds obtained here are not achievable using the Cooper-Presburger procedure).