An Intuitionisticaly Based Description Logic

ABSTRACT. This article presents iALC, an intuitionistic version of the classical description logic ALC, based on the framework for constructive modal logics presented by Simpson and related to description languages, via hybrid logics, by dePaiva. This article corrects and extends the presentation of iALC appearing in \cite{PHR:2010}. It points out the difference between iALC and the intuitionistic hybrid logic presented in \cite{depaiva2003}. Completeness and soundness proofs are provided. A Sequent Calculus for iALC and a discussion on the computational complexity is taken. It is worth mentioning that iALC is used to formalize legal knowledge, and in fact, was specifically designed to this goal.