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
Chapter 2, 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 from atomic
formulae using quantification (over sorted variables) and logical
connectives. 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. Implication may be taken as
primitive
[CHANGED:] (in the presence of an always-false formula),
[] the other connectives being regarded as derived.
The atomic formulae are:
- 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.
Definedness assertions may be derived from existential equations
using conjunction, or regarded as applications of fixed predicates.
Strong equations may be derived from existential equations, using
[CHANGED:] implication and conjunction;
existential equations may be derived from conjunctions of
[] strong equations and definedness assertions, or regarded as
applications of fixed predicates.
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. 4
CoFI
Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
Comments to cofi-language@brics.dk