© 1994 by Oxford University Press
Original Articles |
Circumscription in Data Logic for Data Type Specification
Pontifica Universidad Catolica de Chile, Escuela de Ingenieria, Departamento de Ciencia de la Computacion Casilla 306, Santiago 22, Chile.E-mail: bertossi{at}ing.puc.cl
In this paper we present a logical specification of data types. This specification is built upon a previously given specification for a data type that we want to extend by introducing new constructing objects and defined operations. The extended data type is specified by superposing a circumscription principle to some specification axioms. Circumscription formalizes in second-order logic some forms of (non-monotonic) common-sense reasoning in knowledge bases. By means of circumscription we separate very clearly the first-order specification language (or axioms) from the specification mechanism. By showing the logical equivalence to Zhang's non-circumscriptive data type specification, we obtain the categoricity of our specification when we start from a categorical specification for the original data type.
Keywords: Data type specification; circumscription; first-order logic; second-order logic; knowledge bases; nonmonotonic reasoning