[DL] Tableaux for ALC Question

[gstoil at image.ece.ntua.gr]

T.Herchenroeder at sms.ed.ac.uk said:

> 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!

Hi Thomas,

First, the definition of a clash-free tableau says that a tableau (or
completion-tree) is clash-free if there does not exist ANY node that contains
a clash; where clash is, ...!So finding a clash in the second branch means
that the whole structure is not clash-free.

But lets see why you are confused. I think that's because you are mixing two
different notions. That is the notion of a branch in the tableaux theory for
FOL and branch in the tableaux theory for DLs. 

Now in FOL branch is applied when disjunctive information exists. Therefor,
since you have disjunction closing one branch does not mean that you are
closing the other. But, in DLs branching is simply meant to give a graphical
representation of the model that has been created so far.

So in your 2nd example if you consider the tableaux to be open then you have
created a model for the formulas {(or (exists, C),(exists, ~C)), (forall, C)}. 

Best,
G. Stoilos

> 
> 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/.  **
> 

--