Sociedad Colombiana de Matemáticas:Publicaciones
Revista Colombiana de Matemáticas
Volumen 31 [2] (1997)Páginas 77-98

A deductive calculus for conditional equational system with built-in predicates as premisas

Mauricio Ayala Rincón
Universidade de Brasília, BRASIL

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.

Codigo AMS. 1991 Primary 68Q65. Secondary 68Q42, 68T15, 03C05, 08A70.

Archivo completo : Formato [PDF] (141 K). Formato [DVI] (544 K).