Distributive agents, illustrated

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.