Go backward to Models
Go up to Basic Concepts
Go forward to Satisfaction
Sentences
The many-sorted terms on a signature Sigma=(S,TF,PF,P) and a
set of sorted variables X are built from:
- variables from X;
- applications of qualified function symbols in
TF u PF to argument terms of appropriate sorts.
We refer to such terms as fully-qualified terms, to avoid
confusion with the terms of the language considered in a later
section, which allow the omission
of qualifications and explicit sorts when these are unambiguously
determined by the context.
An explicitly-sorted term is formed by attaching a sort to a
fully-qualified term of that sort.(3)
For a many-sorted signature Sigma= (S,TF,PF,P) the
many-sorted sentences in Sen(Sigma) are the usual closed
many-sorted first-order logic formulae, built using quantification
(over sorted variables) and logical connectives from the
following atomic formulae:
- applications of qualified predicate symbols p e P to argument
terms of appropriate sorts;
- assertions about the definedness of explicitly-sorted terms;
- existential and strong equations between explicitly-sorted terms of
the same sort.
The sentences Sen(Sigma) also include sort-generation
constraints. Let Sigma=(S,TF,PF, P). A sort-generation
constraint consists of (S',F') with S' C S and F'
C TF u PF.
CoFI Tentative Document: LanguageSummary --Version 0.95-- March 6, 1997.
Comments to cofi-language@brics.dk