Information Technology Reference
In-Depth Information
2QWRORJ\
UHGHVLJQ
'HEXJJLQJ
3UHSURFHVVLQJ
,QIHUHQFH
5HDVRQLQJ
2SWLPL]DWLRQ
Fig. 1. Ontology design
existing diagnostic engine, so it can be seen as an "add-on" or refinement of a debugging
system.
3. Fine-grained axiom diagnosis
In order to generalize diagnostic methods to fine-grained axiom diagnosis, we review
the concepts behind model-based diagnosis. This prepares the ground for the diagnostic
algorithm that concludes this section. The workflow when designing and debugging an
ontology is briefly sketched in figure 1. Our focus in this section will be on debugging.
We assume the reader familiar with the resolution principle and predicate and propositional
logic. For convenience, however, we will briefly review some basics and results before going
into technical details (see (de Wolf & Nienhuys-Cheng, 1997, Chapter 2) for full details).
Let
is an assignment of the variables
to values from a given domain, and an assignment of predicates over this domain to
truth-values, such that
ψ
be a first-order logic formula. An
interpretation
of
ψ
ψ
(
Σ
)
becomes true. We write lit
for the set of literals appearing in
either a formula
Σ
or a set
Σ
of formulas. For a set of formulas
Σ
,a
model
is an interpretation
such that every
ψ
∈
Σ
is true. Let
Σ
be a set of formulas and let
ψ
be a formula. We say that
Σ
|
=
ψ
Σ
logically implies
ψ
, writing
, if every model of
Σ
is also a model of
ψ
. For sets of
formulas, we write
.
A
clause
is basically a logical disjunction of literals. Let two clauses
C
1
=
Σ
|
=
Γ
,if
Σ
|
=
ψ
for every
ψ
∈
Γ
L
1
∨
...
∨
L
m
and
C
2
=
M
n
be given and assume that there are two terms
L
i
and
M
j
that can be unified
with each other such that
L
i
=
¬
M
1
∨
...
∨
∨
C
2
, having
the terms
L
i
and
M
j
omitted. For the upcoming results, it is not necessary to fully introduce
the concept of clauses and resolution, and we will confine ourselves to the following informal
example of resolution: assume that we know that Peter plays either chess or football (clause
C
1
). In addition, we know that he does not play chess (clause
C
2
). We conclude that he must
play football (the resolvent is thus
C
1
M
j
. The
resolvent
of
C
1
,
C
2
is the expression
C
1
C
2
without the assertion of Peter playing chess).
For a clause
C
, we say that it can be
derived
from a set
∨
Σ
, if there is a finite sequence of clauses
=
R
1
,...,
R
n
C
such that each clause
R
i
is either in
Σ
or a resolvent of two (previous) clauses
Σ
R
j
,
R
k
with
j
,
k
<
i
. In that case, we write
r
C
.
Finally, we denote the empty clause as
, and note that a set of sentences is
inconsistent
,ifit
models the empty clause. Hence, writing
⊥
Σ
|
=
⊥
is equivalent to saying that a contradiction
is derivable from
Σ
.
Search WWH ::
Custom Search