[DL] Tableaux for ALC Question

[Ian Horrocks]

On 18 Jul 2006, at 19:14, T.Herchenroeder at sms.ed.ac.uk wrote:

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

This is where you have gone wrong. The algorithm says that the input 
concept is satisfiable iff a complete and clash free tree can be 
constructed. The tree you describe has a clash in the label of y2. As 
Franz Baader said in another email, you are introducing notions from 
other algorithms where the tree is used to represent the search space 
that results from non-deterministic inference rules, which is *not* 
what happens here. If you look at the example that follows the 
description of the ALC algorithm, you will see that in this algorithm 
the search involves simple backtracking, saving and restoring the tree 
as necessary.

Ian

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