Atribución-NoComercial 4.0 InternacionalAyala-Rincón, Mauricio2019-06-282019-06-281997https://repositorio.unal.edu.co/handle/unal/43661Conditional 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 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.application/pdfspaDerechos reservados - Universidad Nacional de Colombiahttp://creativecommons.org/licenses/by-nc/4.0/A deductive calculus for conditional equational systems with built-in predicates as premisesArtículo de revistahttp://bdigital.unal.edu.co/33759/info:eu-repo/semantics/openAccessAlgebraic specificationrewriting systemstheorem proving