Models and Theories
This chapter deals with several theories derived from a Horn clause specification. Each theory is complete with respect to a subclass of Mod(SIG,AX) (cf. Section 2.3). Different theories represent different concepts of semantical abstraction. Some of them correspond to the theory of a single SIG-structure, say B. Vice versa, if we start out from a SIG-structure A as the formalization of a data type, an axiom set AX is called correct w.r.t. A if A coincides with B.
KeywordsPredicate Symbol Horn Clause Ground Term Ground Atom Ground Instance
Unable to display preview. Download preview PDF.