Information Technology Reference
In-Depth Information
and
rhs
. Since the literals
X
i
were auxiliary and introduced merely for
the decomposition, the literal
X
4
can be unhesitatingly deleted. This results in a simplified set
(
C
)=
{
X
2
,
X
3
,
X
4
,
B
}
C
simplified
=
{
X
1
→
X
2
∧
X
3
,
X
2
→
B
,
X
3
→¬
B
}
,
which is still inconsistent for the same reasons as
C
is.
3.3 The axiom diagnosis algorithm
With all these preliminaries, the axiom pinpointing algorithm is essentially a standard
diagnosis with preprocessing. It comprises two stages:
=
i
=
1
ζ
(
A
i
)
1. Decompose the given set of axioms
A
1
,...,
A
n
irreducibly into the set
KB
.
2. Run a standard diagnosis on
KB
.
It is known that diagnosis is a computationally hard problem (due to the need of reasoning
for computing the conflict sets and the computation of hitting sets, which is an NP-complete
problem in general Garey & Johnson (1979)). While the algorithm above has been stated
previously in Friedrich et al. (2006), this preliminary work does not exploit the potential
simplification provided by proposition 3.3, by instantly drawing away the attention from
literals that cannot contribute to the inconsistency.
The idea of decomposing an axiom into (irreducible) sub-axioms permits controlling the
granularity as well as the scope of the diagnosis most easily.
Controlling the granularity:
We are free to define the production rules of the underlying
grammar in such a way that more complicated axioms can be generated in one blow.
A simpler, yet equally effective, approach is backsubstituting a selection of irreducible
axioms, thus creating more complicated expressions, yet remaining structurally simpler
than the original axiom. Returning to the previous example, one could backsubstitute
some of the axioms in the decomposition (2) in order to obtain the (logically equivalent but
less fine-grained) decomposition
{
X
0
→
X
1
,
X
0
≡
p
(
X
2
)
,
X
2
≡
A
,
X
1
≡
X
3
∨
X
4
,
≡
∧
≡
(
)
≡
(
)
≡
(
)
}
X
3
X
5
X
6
,
X
5
q
A
,
B
,
X
6
r
B
,
X
4
s
A
.
Diagnosing the latter decomposition obviously provides us with less precise information
than diagnosing the full decomposition (2).
Controlling the scope:
If some parts of the axiom are correct beyond doubt, then we can
simply shift these to the background theory
when running the diagnostic engine. Hence,
the scope comprises all axioms in
KB
, explicitly excluding those in
B
B
.
Example:
Reiter's diagnostic algorithm, when applied to the example ontology given in
section 3.1 returns the following three diagnoses:
1.
D
1
=
{
A
3
→
A
4
∧
A
5
}
=
{
→∀
∧
}
2.
D
2
A
4
s
:
F
C
}
which just says that we may change one of three axioms in order to achieve a repair. Taking
the first of these diagnoses
D
1
and performing axiom-diagnosis on a decomposition of the
axiom provides us with the following diagnoses (among others):
3.
D
3
=
{
A
5
→∃
s
:
¬
F
Search WWH ::
Custom Search