Go up to 2.3 Predicate LogicGo forward to 2.3.2 Atomic Formulas |

The meaning of a term therefore depends on the domain; changing the domain also changes the meaning of a term.

**Operational Interpretation**
In the Logic Evaluator, every term is an instance of a Java class that
implements the following interface:

public interface Term { Value eval() throws EvalException; }

For every `Term`

`t`, the evaluation of

returns the value denoted by `t`.eval()`t` (or throws an exception if some error
has occurred).

A *variable * *assignment (Zuweisung, Belegung)* maps every variable
to a value of the domain.

The value of a variable therefore depends on a given assignment, e.g. the
assignment [`x` |-> "one", `y` |-> "two"] on the
domain of natural numbers maps the variable `y` to the value "two".

Please note that variables may be only mapped to values, i.e., to
*first order objects (Objekte erster Ordnung)*, not to relations or
functions, i.e., to *higher order objects (Objekte höherer Ordnung)*.
The version of predicate logic that imposes this restriction is called
*first order predicate logic (Prädikatenlogik erster Stufe)*. As we will
see in Chapter *Sets*, we can encode functions and relations as
first order objects, such that this restriction does not limit the
expressiveness of the language from the practical point of view.

We call a function constant of arity 0 an *object
constant (Objektkonstante)*.

We use the notion *name* for any combination of characters ("x_2") or
symbols ("sqrt( )"). Since both variables and function constants are
names, we apply in this document the syntactic convention that only names
starting with the letters `x`, `y`, `z` denote variables
(unless explicitly stated otherwise).

- 0, 1, 3.14, "Wolfgang Schreiner", "Austria", pi (object constants);
- | |, sin(), sqrt( ), "mother of" (unary constants);
- +, o , [ ] (binary constants);

Terms are then constructed as follows.

- Every variable is a term.
- If
*fc*is a function constant of arity`n`and`t`_{0}, ...,`t`_{n-1}are terms, then*fc*(`t`_{0}, ...,`t`_{n-1})*elementary term (elementarer Term)*or*function application (Funktionsanwendung)*.

Terms do not necessarily appear in the "standard form" denoted above but they may appear in various syntactic formats.

- 0, "Wolfgang Schreiner", pi (constant terms);
- sqrt(2), sin(
`x`), sum(2,`s`), "the mother of Thomas" (prefix terms); - |1|,
`a`o`b`,`a`[`i`], 1+2 (infix terms);

the roof of the house of her fathercan be written in prefix form as

roof(house(father(she)))with function constants "roof", "house", "father" and a variable "she".

- If
`t`is a variable, then its meaning is the value to which the variable is mapped by the assignment. - If
`t`is an elementary term*fc*(`t`_{0}, ...,`t`_{n-1}), then its meaning is the result of the application of the function`f`denoted by the function constant*fc*to the values of the terms`t`_{i}for the given assignment.

The value of a term therefore depends on the domain (determining the

In the domain "natural numbers" with object constant 0 interpreted as the number "zero", the function constant + interpreted as addition and under the variable assignment [x+ (y+ 0).

In the domain "character strings" with object constant 0 interpreted as the
empty string, the function constant + interpreted as string concatenation
and under the variable assignment [`x` |-> "hi, ", `y`
|-> "babe"], the value of the term is "hi, babe".

The Logic Evaluator has the domain "natural numbers" builtin with object
constants `0`

, `1`

, ...and function constants
`+`

and `*`

. Since terms must be entered always in prefix notation,
terms can be evaluated as follows:

**Operational Interpretation** Elementary terms are implemented by
the following Java class:

The Java termpublic final class Application implements Term { private String name; private Term[] arguments; public Application(String _name, Term[] _arguments) { name = _name; arguments = _arguments; } public Value eval() throws EvalException { Function function = Model.getFunction(name, arguments.length); if (function == null) throw new EvalException("unknown function " + name + "/" + arguments.length); Value[] values = new Value[arguments.length]; for (int i=0; i< values.length; i++) values[i] = arguments[i].eval(); return function.apply(values); } }

`new Application(``f`, *args*).eval()

evaluates to the meaning of the term `Model`

), then we evaluate the arguments
and apply the function to the results.
The operational interpretation of variables will be explained in
Section *Quantified Formulas*.

Author: Wolfgang Schreiner

Last Modification: October 4, 1999