The following illustrates how deduction (backward-chaining) is performed. Forward-chaining works very similarly. I have left out how the agents find others to answer queries -- this is the routing strategy which is an optimization problem.
Agent2 performs only one step, namely, the resolution of:
- P\/Q (the query Agent2 is being asked)
with - ~P\/Q (the rule that Agent2 has in its KB)
This is another illustration, using a common-sense example:
By the way, the implication statement "A implies B":
nice(X) ← sandals(X)
is classically equivalent to "not A or B":
~sandals(X) \/ nice(X)
and therefore it can be resolved with
nice(matt)
by the substitution { X / matt }, yielding the resolvent:
sandals(matt).
This is why the resolution step works.
