Information Technology Reference
In-Depth Information
with a divide-and-conquer approach, and we refer the reader to the Q
UICK
X
PLAIN
-algorithm
by Junker (2004) for that matter.
Returning to the example, for illustrative purposes, one conflict for the ontology is found as:
=
{
A
A
4
,
A
C
3
,
}
.
5
Removing the set
C
from the ontology makes everything consistent again.
It is easy to
construct examples where other conflicts can be found as well.
Computing a diagnosis then amounts to computing a hitting-set for the collection of all
conflicts that exist within
KB
. This is basically theorem 4.4 in Reiter (1987). This is not
surprising and easily justified intuitively: assume
D
to be a hitting-set for the set of minimal
conflicts. Then retracting
D
from
KB
will reduce every conflict set by at least one element,
thus destroying the conflict because those sets are minimal. Since this approach to diagnosis
has seen widespread implementation and many appropriate systems are in place, we leave
the details of the computation aside and concentrate on the problem of axiom pinpointing,
which arises from a shortcoming of the so-far described method.
3.2 Pinpointing erroneous parts of an axiom
Despite the elegance of the existing diagnosis theory, its accuracy is limited to pointing
towards entire axioms. Hence these can be rather complicated and lengthy, which makes
the actual debugging process, i.e. finding the replacement
EX
(cf. definition 3.1) actually
hard. Consequently, we would like to extend the scope of diagnosis to the smallest building
blocks of the sentences within
. This problem is known as
axiom diagnosis
. The trick is using
the syntactical structure of a sentence to decompose a complicated axiom into a sequence of
simple axioms representing only single logical connectives, quantifiers, etc. We will call this
an
irreducible decomposition
, and the whole process of axiom pinpointing then boils down to
diagnosing such an irreducible decomposition of the axiom to be debugged. We will expand
the details in this section, strongly drawing from the work of Friedrich et al. (2006), whilst
presenting further theoretical results that do not appear in this reference.
To ease technicalities in the following, we need two technical yet mild assumptions:
• axioms obey a non-ambiguous formal grammar
G
, such that every application of a
production rule produces only
one
new logical connective or quantifier in each step of
the derivation. We denote the language induced by the grammar
G
as
L
φ
(
G
)
, and assume
, i.e. it is generated by
G
in a non-ambiguous manner.
Although the ambiguity decision problem is undecidable for general grammars, those
permitting disambiguation by lookahead tokens are provably unambiguous and thus
suitable for our needs.
• the
open world assumption
states that a proposition is true if it can be proven, and assumed
to be false if it can be disproved. Any non-present proposition remains unknown until
proven to be true or false. In other words, reasoning under the open-world assumption
demands first making choices before deducing anything.
Our first result formally captures the observation that the parse-tree of an axiom naturally
yields a decomposition that only consists of axioms of the simplest possible form.
Let
A∈
L
(
G
)
for every axiom
A
A
be an axiom with its associated parse-tree. As an example, the axiom
A
→
(
B
∧
C
)
∨
D
can be decomposed into
ζ
(
A
)=
{
A
→
X
1
∨
X
2
,
X
1
→
X
3
∧
X
4
,
X
3
≡
B
,
X
4
≡
C
,
X
2
≡
D
}
.
Search WWH ::
Custom Search