Constructive Description Logic Hybrid-Style

Abstract:

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.

Downloads:

• full text
• slides

BibTeX:

@inproceedings{publication-46,
  author = {dePaiva, Valeria and Haeusler, Edward Hermann and Rademaker, Alexandre},
  title = {Constructive Description Logic Hybrid-Style},
  booktitle = {Pre-Proceedings of International Workshop on Hybrid Logic and Applications},
  year = {2010},
  pdflink1 = {/files/hylo-2010.pdf},
  slides = {/files/hylo-2010-slides.pdf},
  address = {Edinburgh},
  file = {:http://www.floc-conference.org/:TYPE}
}