Next: Appropriate States and
Up: Static Algebras and
Previous: Universes
Terms are defined recursively, as in first-order logic:
-
A variable is a term.
- If f is an r -ary function name and
are terms,
then f() is a term.
As usual, ground terms are terms without variables. By analogy,
other syntactical objects without variables will be called ground.
Atomic Boolean terms are terms of the form
f(![[t]](tbar.xbm)
),
where f is a relation name. Boolean terms are built from atomic Boolean
terms by means of the Boolean operations.