Operators can be represented as functions that change states into new
&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:
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.
Contents    Page-10    Prev    Next    Page+10    Index