@Book{SR--93--95,
year={1993},
author={Claus-Peter Wirth
and Bernhard Gramlich\protect\index{Gramlich, Bernhard}
and K{\"u}hler, Ulrich
and Prote, Horst},
title={Constructor-Based Inductive Validity in Positive/Negative-Conditional Equational Specifications},
publisher={{SEKI Publications}},
series={{SEKI-Report SR--93--05~(SFB) (ISSN 1437--4447)}},
address={FB Informatik, Univ. Kaiserslautern},
abstract={We study algebraic specifications given by finite sets $R$ of positive/negative-conditional equations (i.e.\ universally quantified first-order implications with a single equation in the succedent and a conjunction of positive and negative (i.e.\ negated) equations in the antecedent). The class of models of such a specification $R$ does not contain in general a minimum model in the sense that it can be mapped to any other model by some homomorphism. We present a constructor-based approach for assigning appropriate semantics to such specifications. We introduce two syntactic restrictions: firstly, for a condition to be fulfilled we require the evaluation values of the terms of the negative equations to be in the constructor sub-universe which contains the set of evaluation values of all constructor ground terms; secondly, we restrict the constructor equations to have ``Horn''-form and to be ``constructor-preserving''. A reduction relation for $R$ is defined, which allows to generalize the fundamental results for positive-conditional rewrite systems, which does not need to be noetherian or restricted to ground terms, and which is monotonic w.r.t. consistent extension of the specification. Under the assumption of confluence, the factor algebra of the ground term algebra modulo the congruence of the reduction relation is a minimal model which is (beyond that) the minimum of all models that do not identify more constructor ground terms than necessary. To achieve decidability of reducibility we define several kinds of compatibility of $R$ with a reduction ordering and present a complete critical-pair test a la Knuth-Bendix for the confluence of the reduction relation.},
}