Operators can be represented as functions that change states into new
states:
&forall x &forall y &forall s [¬ On(Monkey, Box, s) &and
At(Monkey, x, s) &and At(Box, x, s) &rarr
At(Monkey, y, pushbox(x, y, s)) &and At(Box, y, pushbox(x, y, s)) ]
pushbox is a function from states to states.
If we pose a question of ``How can the monkey get the bananas?'' and
negate it, we will have ¬ Has(Monkey, Bananas, s) (``There is no
possible state in which the monkey has the bananas.'') After proving
and using answer extraction, we will have an answer such as:
Has(Monkey, Bananas,
grasp(climbbox(pushbox(b, c, goto(a, b, s0)))))
Note that the instruction set of any CPU could be axiomatized as a state space; thus, any computation can be expressed in predicate calculus. In fact, binary Horn clauses have the power of a Turing machine.