A deductive calculus for conditional equational systems with built-in predicates as premises

Conditional equationally defined classes of many-sorted algebras, whose premises are conjunctions of (positive) equations and builtin predicates (constraints) in a basic first-order theory, are introduced. These classes are important in the field of algebraic specification because the combination of...