I have to check whether the following ontology is correct using the ALC tableux algorithm.
A ⊑ ∃s.¬B
C ⊑ A ⊓ B
C(x)
C(y)
s(x,y)
So first i use C ⊑ A ⊓ B to label x and y with A and B. So x and y now have the lables A,B and C. Then i use the ⊑-rule for A ⊑ ∃s.¬B:
¬A ⊔ ∃s.¬B
Since ¬A cant be true for x and y, ∃s.¬B musst be true. So i use ∃-rule that says that if there is no successor of s with label ¬B you add this node. So there is now a node e.g. z that is a sucessor of x and y and has the label ¬B.
Am i right with appyling the ∃-rule here? So in my conisderations the ontology is consistent.
Yes, the ontology is consistent. Your application of ∃-rule is almost correct in that yes, you need to introduce a new named individual as s-successor of x, say z - as you have done. And you have to also introduce a new named individual as s-successor of y, say w.
Thus, you have to introduce 2 new named individuals. You cannot reuse an introduced named individual as successor for 2 different individuals. The reason for this is that in a larger ontology, x and y may have other assertions or axioms that place additional constraints on them which may cause an inconsistency if you assume they have the same s-successor.