Prev Up
Go backward to 1.3 Sentences
Go up to 1 Basic Concepts

1.4 Satisfaction

The satisfaction of a sentence in a structure M is determined as usual by the holding of its atomic formulae w.r.t. assignments of (defined) values to all the variables that occur in them, the values assigned to variables of sort s being in sM. The value of a term w.r.t. a variable assignment may be undefined, due to the application of a partial function during the evaluation of the term. Note, however, that the satisfaction of sentences is 2-valued [CHANGED:] (as is the holding of open formulae with respect to variable assignments). []

The application of a predicate symbol p to a sequence of argument terms holds in M iff the values of all the terms are defined and give a tuple belonging to pM. A definedness assertion concerning a term holds iff the value of the term is defined (thus it corresponds to the application of a constantly-true unary predicate to the term). An existential equation holds iff the values of both terms are defined and identical, whereas a strong equation holds also when the values of both terms are undefined.

The value of an occurrence of a variable in a term is that provided by the given variable assignment. The value of the application of a function symbol f to a sequence of argument terms is defined only if the values of all the argument terms are defined and give a tuple in the domain of definedness of fM, and then it is the associated result value.

A sort-generation constraint (S',F') is satisfied in a Sigma-model M if the carriers of the sorts in S' are  generated by the function symbols in F'. I.e., every element of each sort in S' is the value of a term built from just these symbols (possibly using variables of sorts not in S', with appropriate assignments of values to them).

CoFI Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
Comments to

Prev Up