Information Technology Reference
In-Depth Information
3.1 The general diagnosis problem
The theory of diagnosis as employed in this work is based on the seminal paper of Reiter
(1987), with corrections made by Greiner et al. (1989). The method devised in the sequel
proves axiom pinpointing to be a mere special case of standard diagnosis, except for some
preprocessing. Hence, competing alternative approaches to the same problem, such as
contrived by Schlobach &Cornet (2003) for instance, are technically interesting but come at the
disadvantage of calling for intricate extensions to a diagnostic engine. Our approach comes at
negligible additional computational cost, as we will need a parser for the axiom syntax (which
cannot be avoided anyway).
To reason within an ontology is the process of deriving assertions about individuals from
known facts and rules. Occasionally, we have certain facts and rules in
φ
that are undoubtedly
⊆ φ
correct and consistent, and we collect these in a set
B
, calling it the
consistent background
theory
. These are explicitly excluded from the diagnostic process. The remainder
KB
B
is the set of facts and rules that are subject to the diagnosis. An ontology is usually verified by
testing it against positive and negative test-cases.
Informally, a
diagnosis D
is a minimal set of components whose replacement will create a
consistent ontology. This has been formally captured by Friedrich & Shchekotykhin (2005),
and is clearly defined in
=
φ
\
KB
,
B
,
TC
+
,
TC
−
)
(
Definition 3.1
(Diagnosis (Problem))
.
A
diagnosis problem
is a quadruple
,
where KB is an ontology, comprising a set of facts and rules to be diagnosed, B is a consistent set of facts
and rules (called the
background theory
, and TC
+
and TC
−
are positive and negative test-cases. A
diagnosis
D
⊂
KB is a minimal set (in terms of the subset-relation) of sentences such that there is an
extension EX, where EX is a set of logical sentences added to KB, such that
1.
∪
e
+
|
=
⊥
e
+
∈
TC
+
:
∀
(
KB
\
D
)
∪
B
∪
EX
,
∪
e
−
|
=
⊥
e
−
∈
TC
−
:
2.
∀
(
KB
\
D
)
∪
B
∪
EX
.
Rephrasing this definition, in essence it states that by replacing the components in the
diagnosis
D
with the components in
EX
makes the ontology
φ
consistent with every positive
test-case and inconsistent with every negative test-case.
Example:
for illustration, consider the following example ontology:
A
1
:
A
1
→¬
A
∧
A
2
∧
A
3
A
2
:
A
2
→¬
D
∧
A
4
A
→
A
4
∧
A
4
:
A
4
→∀
∧
3
:
A
3
A
5
s
:
F
C
A
→∃
¬
A
→
∧
5
:
A
5
s
:
F
6
:
A
6
A
4
D
The inconsistency is revealed by the following reasoning, starting with
A
1
as a known fact:
from
A
1
, we can deduce (among others) the assertion that
A
3
holds true. This one in turn
implies the validity of
A
4
and
A
5
via rule
3
.Yet
A
4
tells that all individuals
s
enjoy property
F
, while
A
5
implies that there is at least one individual that does
not
fall into the class
F
. This
inconsistency is to be removed with the aid of diagnosis.
The problem tackled in the following is motivated by the (initially made) observation that the
process will not remain that simple in a real-life ontology. Facing very complicated axioms,
the diagnostic algorithms inspired by the work of Reiter (1987), essentially provide rather
coarse-grained pointers towards the error. We shall improve on this.
Computing a diagnosis relies on the concept of
conflict sets
as introduced by de Kleer (1976)
and adapted by Reiter (1987). Given a diagnosis problem
A
KB
,
B
,
TC
+
,
TC
−
)
(
,a
conflict set
C
B
is inconsistent (either by itself or with any of the test-cases). A
conflict is said to be minimal, if no subset of
C
is a conflict. Computing conflict sets can be done
⊆
KB
is such that
C
∪
Search WWH ::
Custom Search