[DL] Tableaux for ALC Question

[Franz Baader]

>        {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?

What you appear to mix up here are the two kinds of trees generated
by such a tableaux algorithm:
- the search tree due to non-deterministic branching
  (in the ALC case: the disjunction rule)
- the tree-model that the algorithm is trying to generate

In the first tree, one needs a clash in every branch, but in the second
it is enough to have just one clash to indicate unsatisfiability. Thus,
in your example, the fact that you find a clash {C,~C}(y2) is enough
for the algorithm to say unsatisfiable.

To avoid this confusion, I prefer to describe these algorithms as
working on sets of ABoxes rather than the more traditional tableaux
representation where both kinds of trees are mixed (see, for example,
my concrete domains paper with Hanschke
http://lat.inf.tu-dresden.de/research/papers/1991/DFKI-RR-91-10.ps.gz
or my DL tutorial
http://lat.inf.tu-dresden.de/~baader/Talks/dl2.pdf)

Best regards,

-Franz Baader