Go backward to 1.2 Models
Go up to 1 Basic Concepts
Go forward to 1.4 Satisfaction
1.3 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
fully-qualified
terms;
- existential and strong equations between
fully-qualified
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: CASL/Summary-v0.97 --Version 0.97-- 20 May 1997.
Comments to cofi-language@brics.dk