Inductive Proofs in Specifications Parametrized by a Built-in Theory

Abstract

We consider the problem of proving hypotheses to be valid in all canonical term models of some parametrized positive/negative conditional equational specification that are induced by the actualizations of the given parameter theory. In a first part we develope a method to operationally handle as well the parameter actualizations as the body specification and here in particular the negative conditions occuring possibly in the conditional equations. By introducing restrictions on the conditional equations the induced canonical term algebras become in a certain sense initial models of the specification. In a second part we present a proof by consistency method to deal with hypotheses formulated as clauses over the body and (formal) parameter language. If some syntactical premises are fulfilled and if a (built-in) algorithm is available that decides whether clauses over the parameter language only are logical consequences of the parameter theory or not, then the proof method becomes refutationally complete.