The Relevance of Constructors

Abstract

Refinements of paramodulation (cf. Section 5.3) such as goal reduction (cf. Chapter 7) and narrowing (cf. Chapter 8) are complete only if certain requirements on <SIG,AX> are fulfilled, which, in turn, depend on the division of <SIG,AX> into a base specification <BSIG,BAX> and the rest of <SIG,AX>. The base signature BSIG contains all sorts, predicates and sort-building or constructor functions of SIG. Hence the remaining part of SIG consists of operation symbols called non-constructor or, with the name indicating their meaning,destructor, inquiry, state-transition or value-returning functions. Accordingly, BAX specifies the predicates, in particular the equality predicates, with the help of constructor functions. Non-base axioms must be conditional equations and should only be used to specify non-constructor functions.