Equivalence and difference between institutions: simulating Horn Clause Logic with based algebras
- 1 June 1995
- journal article
- research article
- Published by Cambridge University Press (CUP) in Mathematical Structures in Computer Science
- Vol. 5 (2) , 189-215
- https://doi.org/10.1017/s0960129500000712
Abstract
In this paper, we investigate several logical frameworks whose expressiveness lies between Conditional Equational Logic and Horn Clause Logic. The main result deals with thePART-construction, which interprets total based algebras as partial algebras. This construction can be viewed as a simulation of Horn Clause Theories by means of Conditional Equational Theories. Other constructions in other frameworks are extendable to simulations in a similar way. The notion of categorical retractive simulation captures some essential properties of these, which allows us to measure the equivalence and difference between institutions.Keywords
This publication has 20 references indexed in Scilit:
- Consistency of equational enrichmentsPublished by Springer Nature ,2005
- A hierarchy of institutions separated by properties of parameterized abstract data typesPublished by Springer Nature ,1995
- Institutions: abstract model theory for specification and programmingJournal of the ACM, 1992
- Equational type logicTheoretical Computer Science, 1990
- Models of Horn theoriesContemporary Mathematics, 1989
- Specifications in an arbitrary institutionInformation and Computation, 1988
- Partial algebras flow from algebraic specificationsPublished by Springer Nature ,1987
- On the existence of free models in abstract algebraic institutionsTheoretical Computer Science, 1985
- Partial algebras—survey of a unifying approach towards a two-valued model theory for partial algebrasAlgebra universalis, 1982
- Partial abstract typesActa Informatica, 1982