Go up to 2.3 Predicate Logic Go forward to 2.3.2 Atomic Formulas

2.3.1 Terms

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 t.eval() returns the value denoted by 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₀, ..., t_n-1 are terms, then

  fc(t₀, ..., t_n-1)

  is a term, called an  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 father

roof(house(father(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₀, ..., 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.

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:

public 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);
  }  
}

The operational interpretation of variables will be explained in Section Quantified Formulas.