ALC

Propositional Logic is not expressive enough as there are no quantifiers. So we try to use First-Order Predicate Logic. This however is too expressive and this algorithms are too complex and don't terminate. So the idea is to have a logic that is more expressive than Propositional Logic but weaker than First-Order Predicate Logic.

Concept Role

Syntax

Grammar for ALC:

Concept Definition work here too. We can also do Normalization of Concept Definition, which can get exponential for cyclic/recursive definitions.

Semantics

Interpretation Function $[[\circ]]$

or alternitavely via Translation into First-Order Predicate Logic by extending the translation with these rules:

These rules more or less guard away formulae which would make ALC undecidable.

Some Identities:

Use these identities to formulate the Negation Normal Form

We define assertions for ALC:

• $a:\varphi$ → $a$ is a $\varphi$
• $\text{a R b}$ → $a$ stands in relation $R$ to $b$

These make up the ABox in ALC.

Their semantics are:

We also extend the translation into first order logic:

Inference

ALC Tableau Calculus