[DL] Tableaux for ALC Question

[T.Herchenroeder at sms.ed.ac.uk]

Hi all!

I'm cracking my head over the existential rule for ALC tableaux. For 
reference,
I'll give here a transcription of the version from Ian Horrock's PhD thesis:

exist-rule:
if 1. exist(R,C) is element of L(x) and
    2. there is no y s.t. L(<x,y>) = R and C is element of L(y)
then create a new node y and edge <x,y>
    with L(y) = C and L(<x,y>) = R

(But I believe other formalisations, like Baader, are compatibel).

Now consider the following two simple examples. Let's suppose your 
current node
in the proof looks like

       {exist(R,C),exist(R,~C)}

The concept described by this node should obviously be satisfiable. So if you
apply the exist rule to the first element, you get a new edge R and a new node
{C}. If you take the rule condition literally, you could then apply the exist
rule to the second element, giving you a second new node {~C} with edge 
R. Both
child nodes constitute a model, the tableaux is saturated and at least one
branch is open, which means the initial concept is satisfiable, which is what
one expected. What you do not want to happen is to re-use the R-edge of the
first expansion for the second, and simply add ~C to the first new node (which
would lead to the tableaux being closed, ie. unsatisfiable).

Now, for the second example extend the initial node with a universal:

       {exist(R,C),exist(R,~C),forall(R,C)}

This concept you do *not* want to be satisfiable (there cannot be a 
model where
an individual x has relation R only with members of C, and then demand 
there be
at least one relation to a member of not-C). If you apply the exist 
rule to the
first existential, giving you {C}(y1), and then to the second, giving you
{~C}(y2), and then apply the forall rule, you get {C,~C}(y2) (when applied to
the second R edge; the first is blocked by the rule condition for forall).

The second child node closes in a clash, but the first gives you a 
model, meaning the initial concept is satisfiable - which is not what 
you want!

Where is my mistake? Any hints, also pointers to more appropriate 
lists, are welcome!

Thanks,
=Thomas