Information Technology Reference
In-Depth Information
operation is introduced along with
Resolve
and
Ancestry
operations. With Skip opera-
tion, SOL resolution focuses on deriving only those consequences belonging to the pro-
duction field
P
.
SFK resolution
[8] is based on a variant of ordered resolution, which is
enhanced with Skip operation for finding characteristic clauses. SOL resolution is com-
plete for finding
Newcarc
(
Σ,C,
)
by treating an input clause
C
as the
top clause
and
derives those consequences relevant to
C
directly. SOLAR (SOL for Advanced Reason-
ing) [21,22] is a sophisticated deductive reasoning system based on SOL resolution [12]
and the connection tableaux, which avoids producing non-minimal consequences as
well as redundant computation using state-of-the-art pruning techniques. Consequence
enumeration is a strong point of SOLAR as an abductive procedure because it enables
us to compare many different hypotheses [16].
P
3
Partition-Based Consequence Finding
This section proposes partition-based consequence finding. We start from a review of
the basic terminology and the message passing algorithm between partitioned knowl-
edge bases in [3], whose basic idea is from Craig's Interpolation Theorem [6,24].
3.1
Partitions and Message Passing
=
i≤n
A
i
, in which each axiom set
We suppose the whole axiom set
A
A
i
(
i
≤
n
)
is called a
partition
. We denote as
S
(
A
i
)
the set of (non-logical) symbols appearing in
A
i
.A
graph induced from the partitions
i≤n
A
i
is a graph
G
=(
V,E,l
)
such that (i)
the set
V
of nodes are the same as the partitions, that is,
i
∈
V
iff the partition
A
i
exists;
(ii) the set
E
of edges are constructed as
E
=
{
(
i,j
)
|
S
(
A
i
)
∩
S
(
A
j
)
=
∅}
,thatis,the
edge
(
i,j
)
A
j
; and (iii) the mapping
l
determines the label
l
(
i,j
)
of each edge
(
i,j
)
called the
communication language
between the partitions
∈
E
iff there is a common symbol between
A
i
and
A
j
. In partition-based theorem proving by [3],
l
(
i,j
)
is
initially set to the
common language
of
A
i
and
A
j
)
.
The communication language
l
(
i,j
)
is then updated by adding symbols from some
other partitions when cycles are broken (Algorithm 2). In Section 3.3,
l
(
i,j
)
is further
extended by including the language for consequence finding.
Given the partitions
i≤n
A
i
and its induced graph
G
=(
V,E,l
)
, we now consider
the query
Q
to be proved in the partition
A
i
and
A
j
,whichis
C
(
i,j
)=
S
(
A
i
)
∩
S
(
n
). Given a set
S
of non-logical
symbols, the set of formulas constructed from the symbols in
S
is denoted as
A
k
(
k
≤
L
(
S
)
.
Definition 1 .
For two nodes
i,k
V
, the length of a shortest path between
i
and
k
is
denoted as
dist
(
i,k
)
.Given
k
,wedefine
i
∈
≺
k
j
if
dist
(
i,k
)
<dist
(
j, k
)
.When
k
is
clear from the context, we simply denote
i
≺
j
instead of
i
≺
k
j
. For a node
i
∈
V
,a
node
j
∈
V
such that
(
i,j
)
∈
E
and
j
≺
k
i
is called a
parent
of
i
(with respect to
≺
k
).
In the ordering
≺
k
, the node
k
is called the
root
(with respect to
≺
k
), and a node
i
that
is not a parent of any node is called a
leaf
(with respect to
≺
k
).
