Go backward to 2.3.1 Terms Go up to 2.3 Predicate Logic Go forward to 2.3.3 Equality |
Predicate constants may appear in various syntactic formats.
We now introduce formulas that allow us to express properties about objects.
pc(t0, ..., tn-1)is a formula, called atomic formula (atomare Aussage).
Atomic formulas may appear in various syntactic formats.
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).
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:
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 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.