[DL] Question on ALC dl

[Fabio Cozman]

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