Recently, there has been a growing interest in constructive reinterpretations of description logics. This has been motivated by the need to model in the DLs setting problems that have a consolidate tradition in constructive logics. In this paper we introduce a constructive description logic for the language of ALC based on the Kripke semantics for Intuitionistic Logic. Moreover we give a tableau calculus and we show that it is sound, complete and terminating.
['Loris Bozzato', 'Mauro Ferrari', 'Camillo Fiorentini', 'Guido Fiorino']
A decidable constructive description logic