On translating partial to total specifications with applications to theorem proving for partial specifications

Abstract

In this paper it is shown how partial specifications (with strong equations) can be translated into total ones. This translation is proven to be sound and complete, in the sense that a theorem is valid for all models of the partial specification if and only if its translation is valid in all models of the total one. Specifications are assumed to include the booleans built-in. The results obtained allow to use contextual rewriting as a proof method for partial specifications in which conditional equations are restricted to have in the premises only boolean terms or definedness conditions. The general case can only be handled with a generalization of contextual rewriting not yet developed. The results, applied to PAnndA-S, allow to handle the use of domain predicates with, both, weak and strong interpretations.