A deductive calculus for conditional equational systems with built-in predicates as premises
Archivos
Autores
Ayala-Rincón, Mauricio
Director
Tipo de contenido
Artículo de revista
Idioma del documento
EspañolFecha de publicación
1997
Título de la revista
ISSN de la revista
Título del volumen
Documentos PDF
Resumen
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 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.