Go backward to 2.3.1 TermsGo up to 2.3 Predicate LogicGo forward to 2.3.3 Equality |

Predicate constants may appear in various syntactic formats.

- "is positive" (unary predicate constant);
- <= , | (binary predicate constants);
- "is father of" (binary predicate constant);
- "is a child of ...and of ..." (ternary predicate constant).

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

is a formula, calledpc(t_{0}, ...,t_{n-1})

Atomic formulas may appear in various syntactic formats.

- "1 is positive";
- 2 <= sqrt(
`x`+3); - 2 | 5;
- "Thomas is the father of Susanne";
- "Susanne is a child of Thomas and of Birgit".

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".

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).

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<= sqrt(y+1)

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:

The Java termpublic 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); } }

`new Atomic(``pc`, *args*).eval()

evaluates
to the meaning of the predicate `Model`

), then we evaluate the arguments
and apply the predicate to the results.
Author: Wolfgang Schreiner

Last Modification: October 4, 1999