previous up next
Go backward to 2.3.1 Terms
Go up to 2.3 Predicate Logic
Go forward to 2.3.3 Equality
RISC-Linz logo

2.3.2 Atomic Formulas

Constants may not only denote functions but also predicates.

Definition 16 (Predicate Constant) A  predicate constant (Prädikatenkonstante) is a name that may represent some predicate. The arity of the predicate constant determines the arity of the predicates it may stand for.

Predicate constants may appear in various syntactic formats.

Example  The following are predicate constants:

We now introduce formulas that allow us to express properties about objects.

Proposition 13 (Atomic Formula) If pc is a predicate constant of arity n and t0, ..., tn-1 are terms, then
pc(t0, ..., tn-1)
is a formula, called  atomic formula (atomare Aussage)

Atomic formulas may appear in various syntactic formats.

Example  The following are atomic formulas: A natural language formula
Bill Clinton is a better president than his predecessor.
can be written in prefix form as
isBetterPresident(Bill Clinton, Predecessor(Bill Clinton))
with predicate constant "isBetterPresident" and function constants "Predecessor" and "Bill Clinton".

Definition 17 (Semantics of Atomic Formulas) The meaning of an atomic formula pc(t0, ..., tn-1) under an assignment in some domain is the truth value of the predicate denoted by the predicate constant pc for the values of the terms ti under the given assignment.

The truth value of an atomic formula thus depends on the domain (determining the interpretation of the predicate constant and the interpretation of the function constants in the argument terms) as well as on the variable assignment (determining the values of the variables).

Example  Take the formula
x <= sqrt(y+1)
in the domain of real numbers with ` <= ' interpreted as the "less than or equal" relation, `sqrt( )' interpreted as "square root", `+' interpreted as addition, and `1' interpreted as "one". For assignment [ x |-> 3, y |-> 8], above formula is true; for assignment [ x |-> 4, y |-> 3], it is false.

Now take the domain of points on a plane with ` <= ' interpreted as "is not farther from the zero point than", `sqrt( )' interpreted as "projection of a point to the horizontal axis", `+' interpreted as addition of point coordinates, `1' interpreted as point (1,0). Is the formula true for the assignment [ x |-> (2,2), y |-> (1,1)] or not?

The Logic evaluator has the predicates = and <= on natural numbers built in; all formulas have to be entered in prefix notation:

Operational Interpretation  Atomic formulas are implemented by the following Java class:

public final class Atomic implements Formula
  private String name;
  private Term[] arguments;

  public Atomic(String _name, Term[] _arguments)
    name = _name;
    arguments = _arguments;

  public boolean eval() throws EvalException
    Predicate predicate = Model.getPredicate(name,arguments.length);
    if (predicate == null)
      throw new EvalException("unknown predicate " + name + 
                              "/" + arguments.length);
    Value[] values = new Value[arguments.length];
    for (int i=0; i<values.length; i++)
      values[i] = arguments[i].eval();
    return predicate.apply(values);
The Java term new Atomic(pc, args).eval() evaluates to the meaning of the predicate f(args) (where pc is a predicate constant and args is the list of arguments). As one can see, first we determine the interpretation predicate of the predicate constant in the given domain (Model), then we evaluate the arguments and apply the predicate to the results.
Author: Wolfgang Schreiner
Last Modification: October 4, 1999

previous up next