Information Technology Reference
In-Depth Information
In this work, we consider the problem of
distributed consequence finding
. Conse-
quence finding [18,12,20] is a problem to discover an interesting theorem derivable
from an axiom set, and is a promising method for problem solving in AI such as query
answering [17], abduction [12,16,22], induction [23,13], diagnosis, planning, recogni-
tion and understanding. There are some
complete
procedures for consequence finding
in first-order clausal theories [12,8] and efficient systems have also been developed
[21,22]. Our concern here is to design a complete method in the distributed setting, that
is, to obtain every consequence that would be derived from the whole knowledge base
if it were gathered together. In this paper, we propose two new methods for distributed
consequence finding.
The first method here is a generalization of partition-based theorem proving by [3] to
consequence finding. The whole axiom set is partitioned into multiple sets called
parti-
tions
, each of which can be associated with one agent. In this method, a pair of partitions
must be connected with their
communication language
. The connections between parti-
tions constitute a graph, but cycles must be removed so that the graph are transferred to
a tree. Consequence finding is firstly performed in the leaves of the connection tree, and
its consequences are sent to the parent if they belong to the communication language.
This process is repeated until the root. To get a complete procedure in this method, it is
important to decide the communication languages between two partitions, so we pro-
pose the method to determine them. It should be stressed that, although partition-based
theorem proving by [3] also uses a consequence finding procedure in each individual
reasoning task of an agent, the aim of [3] is not consequence finding from the knowl-
edge base but is used for theorem proving tasks.
The second proposed method is a more cooperative one. In this method, we do not
presuppose graph structures of agents, but any agent has a chance to communicate with
other agents, hence the framework is more dynamic than the first method. Firstly, a
new clause is added to an agent
A
1
, either as a top clause of the given problem or as
a newly sent message from other agents, then triggers consequence finding from that
clause with the axioms of
A
1
. Then, for each such newly derived clause
C
,ifthereisa
clause
D
in the axiom set of another agent
A
2
such that
C
and
D
can be resolved, then
C
is sent to
A
2
and is added there. This process is repeated until no more new clause
can be resolved with any clause of any other agent. We will compare these two methods
and centralized approaches, and discuss the merits and demerits of both methods. We
will also discuss relations with other previously proposed approaches to consequence
finding in distributed settings [14,1,2].
The rest of this paper is organized as follows. Section 2 reviews the background
of consequence finding and SOL resolution. Section 3 proposes partition-based con-
sequence finding. Section 4 proposes a more cooperative algorithm for consequence
finding and Section 5 compares the two proposed approaches. Section 6 discusses re-
lated work, and Section 7 gives a summary and future work.
2
Consequence Finding
In this section, we review consequence finding from an axiom set and a complete proce-
dure for it. The task of consequence finding is related with many AI reasoning problems,
and is indispensable in partition-based theorem proving in Section 3.1 too.
