[DL] Tableaux for ALC Question

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

Thanks to all the posters. That helped a lot!

=Thomas

> 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
>
> ---
> **  You received this mail via the description logic mailing list; 
> for more  **
> **  information, visit the description logic homepage at 
> http://dl.kr.org/.  **
>