Distributed Consequence Finding: Partition-Based and Cooperative Approaches - Agents and Artificial Intelligence - page 429

Fig. 2. Partitions for “Getting Money”

Partition-based theorem proving of [3] cannot be directly applied to consequence find-
ing problems for Q A k ) although [3, Section 2.3] briefly mentions how to apply

their MP algorithm to such a query constructed from languages in different partitions (a
more detailed discussion will be given later in Section 3.3). Hence, we will extend the
partition-based reasoning framework to a complete method for distributed consequence
finding.

∈L (

3.2 Example
We now show an example to see that the partition-based theorem proving method cannot
be directly applied to consequence finding. The problem is to find means to withdraw
money from one's bank account. The intended solution is that one must have either a
cash card or a bankbook, which is represented as card ∨ bankbook . The knowledge

base of this problem consists of the following clauses.
•¬

closed (The bank is closed on holidays.)
•¬weekday ∨ open (The bank is open on weekdays.)
•

holiday ∨

holiday ∨ weekday (Any day is either a holiday or a week day.)

•¬ counter (If one needs money and the bank is

open, then (s)he goes to an ATM or a counter of the bank.)
•¬

need money ∨¬ open ∨ ATM ∨

need money ∨¬ closed ∨ ATM (If one needs money and the bank is closed,

then (s)he goes to an ATM.)
•¬

get money (One cannot get money if (s)he does not have a
cash card at an ATM.)
•¬

ATM ∨ card ∨¬

get money (One cannot get money if (s)he does not
have a bankbook at a counter.)

counter ∨ bankbook ∨¬

• Input facts: need money (One needs money.)

Input facts: get money (One gets money.)
Here we assume that the partitions are constructed as in Fig. 2, in which clauses are
distributed in a scattered way. Algorithm 2 removes the edge (1,3) and then adds ATM
to the labels of other edges. However, the clause card

•

bankbook cannot be deduced
by Message Passing Algorithm 1: since l (1 , 2) and l (1 , 3) do not contain card ,the
clause (1) cannot be resolved with any clause in other partitions. In fact, it is necessary
to resolve all clauses (1) to (7).

∨