[DL] Question on ALC dl
Fabio Cozman
fgcozman at usp.br
Thu Jan 17 15:23:13 CET 2008
Dear DL-members,
I'd be very grateful for any help with two questions concerning
the ALC description logic:
1) Could someone suggest a paper or repository containing a
realistic ontology written in ALC, to be used as example? Thanks!
2) I have a question on the tableau algorithm for
ALC. Consider the usual tableau for verifying satisfiability of a
concept C with an acyclic terminology. The first step is to "unfold"
the terminology: transform all inclusions into definitions, and then
replace defined concepts by their definitions until we reach primitive
concepts (this is described in many places; for instance, in "An
overview
of tableau algorithms for description logics" by Baader and Sattler).
My question is this.
Suppose we have "forall r.D" in the concept C, and
we go unfolding D recursively. Clearly only concepts that are
"upstream"
to D in the terminology will appear, as the terminology is acyclic.
So, I see that if there are clashes with these "upstream" concepts
in the
the terminology, these clashes will be detected by the tableau method
when we consider an individual b that satisfies r(a,b), where
a is
an individual in the tableau.
But "unfolding" never touches the inclusions/definitions that are
"downstream" to D in the terminology (I hope this is clear). So, if
there
are clashes "downstream", they do not appear. Is there a proof somewhere
that the "unfolding" procedure is correct, in the sense that the parts
of the terminology that are "downstream" to D do not matter?
I've found statements in the literature to the effect that these parts
of the terminology do not matter, but I would like to see a proof
or at least a detailed explanation. I apologize if this is a silly
question and the answer is obvious.
Many thanks,
Fabio Cozman
More information about the dl
mailing list