Information Technology Reference
In-Depth Information
Fig. 3.
Updating Communication Languages
Step 1 in Algorithm 3 can be run in parallel for each partition that is most distant from
the root partition. Step 4 can be computed in parallel for each characteristic clause.
For the example in Section 3.2, applying Cycle Cut and the decision method of the
communication language results in Fig. 3. By this way, the clause (1) consists of the
symbols in
l
(1
,
2)
, then can be resolved with other clauses in
A
2
. Applying Algorithm 3,
the intended consequence
card
bankbook
can be obtained.
Termination of Algorithm 3 is guaranteed under some finiteness conditions. For this,
(1) if there is a finite number of cycles in the induced graphs, the maximum depth of a
tree is finite after applying Algorithm 2, and (2) if there are no recursive theories in each
partition, consequence finding in the partition produces a finite number of characteristic
clauses. The second condition is satisfied if ground consequences are only produced and
there are no function symbols in the language.
The correctness of a distributed consequence finding algorithm
A
is defined as fol-
lows. Suppose the whole knowledge base
∨
A
and a production field
P
.
A
is
sound
if any
clause derived by
A
is a logical consequence of
.
A
is
complete
if it
holds for any partitioning of
A
that: for any clause
C
belonging to
Th
P
(
A
and belongs to
P
A
)
,thereisa
clause
D
derived by
A
such that
D
subsumes
C
.
Theorem 2 (Soundness and Completeness of Partition-based Consequence Find-
ing).
=
i≤n
A
i
, its induced graph
G
=
Suppose an axiom set and its partitions
A
(
V,E,l
)
, and a stable production field
A
i
has
a sound and complete algorithm for consequence finding. Then, Algorithm 3 is sound
and complete for distributed consequence finding.
P
=
L
. We assume that every partition
Proof. Any clause derived by Algorithm 3 refers to a subset of
.
Then, soundness follows from the monotonicity of first-order logic. Completeness can
be proved by induction on the length of any clause
C
A
and belongs to
P
∈
Th
P
(
A
)
.When
|
C
|
=1
,let
A
k
be a partition of
A
k
)
. Then, by Theorem 1, a clause
D
subsuming
C
can be derived by Algorithm 3, which works in the same way as Algorithm 1. Suppose
that completeness holds for
A
such that
C
∈L
(
|
C
|≤
m
, and we prove the case of
|
C
|
=
m
+1
.Let
C
=
C
∨
C
|
A
be
.Since
C
belongs
L
,where
|
=
m
and
L
is a literal. Let
A∪{¬
L
}
A
=
i≤n
A
i
)
,
C
∈
A
)
holds. Then, assume a partition
to
P
and
C
∈
Th
P
(
A
Th
P
(
