A deductive calculus for conditional equational systems with built-in predicates as premises
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...
- Autores:
-
Ayala-Rincón, Mauricio
- Tipo de recurso:
- Article of journal
- Fecha de publicación:
- 1997
- Institución:
- Universidad Nacional de Colombia
- Repositorio:
- Universidad Nacional de Colombia
- Idioma:
- spa
- OAI Identifier:
- oai:repositorio.unal.edu.co:unal/43661
- Acceso en línea:
- https://repositorio.unal.edu.co/handle/unal/43661
http://bdigital.unal.edu.co/33759/
- Palabra clave:
- Algebraic specification
rewriting systems
theorem proving
- Rights
- openAccess
- License
- Atribución-NoComercial 4.0 Internacional
| Summary: | 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. |
|---|