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
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 19 references indexed in Scilit:
- A hierarchy of institutions separated by properties of parameterized abstract data types1995
- Institutions: abstract model theory for specification and programmingJournal of the ACM, 1992
- Unifying initial and loose semantics of parameterized specifications in an arbitrary institutionLecture Notes in Computer Science, 1991
- Equational type logicTheoretical Computer Science, 1990
- Models of Horn theories1989
- Specifications in an arbitrary institutionInformation and Computation, 1988
- Partial algebras flow from algebraic specificationsLecture Notes in Computer Science, 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