Constructive modal logics come in several different
flavours and constructive description logics, not
surprisingly, do the same. We introduce an
intuitionistic description logic, which we call iALC
(for intuitionistic ALC, since ALC is the name of
the canonical description logic system) and provide
axioms, a Natural Deduction formulation and a
sequent calculus for it. The system iALC is related
to Simpson’s constructive modal logic IK the same
way Mendler and Scheele’s cALC is related to
constructive CK and in the same way classical
multimodal K is related to ALC. In the system iALC,
as well as in cALC, the classical principles of the
excluded middle (C ⊔\neg C) = ⊤, double
negation \neg\neg C=C and the definitions of the
modalities ∃R.C = \neg ∀R.\neg C and
∀R.C= \neg ∃R.\neg C are no longer
validities, but simply non-trivial TBox statements
used to axiomatize specific application
scenarios. Meanwhile in iALC, like in classical ALC,
we have that the distribution of existential roles
over disjunction i.e. ∃R.(C ⊔D) =
∃R.C ⊔∃R.D and (the nullary
case) ∃R. ⊥= ⊥hold, which is not
true for cALC. We intend to use iALC for modelling
juridical Artificial Intelligence (AI) systems and
we describe briefly how.