ALC Tableau Calculus

The ALC Tableau Calculus acts on assertions:

• $x:\phi$
• $\text{x R y}$

where $\phi$ is a normalized Concept in NNF.

We have the following Inference Rules:

In the fourth rule you can see that the Universal Quantifier is guarded by the relation. This is the part where the Standard Tableau Calculus was failing because there we would have to test all possible assertions and not only the ones in the relation.

The last rule basically introduces another witness (Skolem… ).

This calculus is

• sound
• and complete