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 \sf
IK the same way Mendler and Scheele’s c\calALC
is related to constructive \sf CK and in the same
way classical multimodal \sf K is related to \sf
ALC. In the system \ialc, as well as in c\cal
ALC, the classical principles of the excluded
middle C\dlor \neg C= \sf T, 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
\sf ALC, we have that the distribution of
existential roles over disjunction i.e. ∃R.(C\dlor D) = ∃R.C \dlor ∃R.D and
(the nullary case) ∃R.⊥= ⊥hold,
which is \em not true for c\cal ALC. We intend
to use \ialc for modelling juridical Artificial
Intelligence (AI) systems and we describe briefly
how.