The Relevance of Constructors

  • Peter Padawitz
Part of the EATCS Monographs on Theoretical Computer Science book series (EATCS, volume 16)


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.


Base Representation Base Specification Horn Clause Base Theorem Ground Base 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 1988

Authors and Affiliations

  • Peter Padawitz
    • 1
  1. 1.Fakultät für Mathematik und InformatikUniversität PassauPassauGermany

Personalised recommendations