A deductive calculus for conditional equational systems with built-in predicates as premises
Mauricio Ayala Rincón · 1997
Conditional equationally defined classes of many-sorted algebras, whose premises are conjunctions of (positive) equations and built-in predicates (constraints) in a basic first-order theory, are introduced. These classes are important in the field of algebraic specification because the combination of equational and built-in premises give rise to a type of clauses which is more expressive than purely conditional equations. A sound and complete deductive system is presented and algebraic aspects of these classes are investigated. In particular, the existence of free algebras is examined. 1 Introduction The need to use conditional equations appears firstly in universal algebra in order to represent some algebraic structures, for example the left cancellative law can be expressed by the conditional equation x y = x z =) y = z. Classes of algebras presented by equations and conditional equations are called varieties and quasivarieties (or positive equational universal Horn classes), res...