Handbook of Automated Reasoning

5.2 Variations of $\mathcal{A}\mathcal{L}\mathcal{B}$

A closer inspection of the formulas we obtain from translating $\mathcal{A}\mathcal{L}\mathcal{B}$ knowledge bases into first-order logic reveals, that only the presence of the top role ∇ and role complement prevents Π(Γ) from being guarded for arbitrary knowledge bases Γ.

5.19. Example

Consider the $\mathcal{A}\mathcal{L}\mathcal{B}$ expressions ∀∇.A and ∀¬P.A. The translation of these expression is (∀y) (T → A(y)) and (∀y) (¬P(x, y) → A(y)), respectively. ...