[DL] Question on ALC dl
fgcozman at usp.br
Thu Jan 17 15:23:13 CET 2008
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
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
to D in the terminology will appear, as the terminology is acyclic.
So, I see that if there are clashes with these "upstream" concepts
the terminology, these clashes will be detected by the tableau method
when we consider an individual b that satisfies r(a,b), where
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
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.
More information about the dl