|Revista Colombiana de Matemáticas|
Abstract. 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 wich 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.Palabras claves. Algebraic specification, rewriting systems, theorem proving.