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,
non-overloaded
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.
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.
An inner quantification over a variable makes a hole in the scope of
an outer quantification over the same variable, regardless of the
sorts of the variables.
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 Document: LanguageSummary --DRAFT, Version 0.96-- 30 April 1997.
Comments to cofi-language@brics.dk