Kripke semantics and tableau procedures for constructive description logics.

In this work we present the decidable constructive description logic KALC: the logic is based on a Kripke-style semantics for the language of the description logic ALC and it is directly inspired by the Kripke semantics for first order intuitionistic logic. We study the constructive properties of this logic and its relations with classical semantics. Then, by means of an example, we show how its semantics is suitable for the description of incomplete and dynamic knowledge. We then introduce a tableau calculus for this logic and we prove its completeness with respect to KALC semantics. Most notably, by proving the completeness and termination results for such calculus, we obtain an effective proof search algorithm for our logic. We also study the relations of KALC with our previous proposals for constructive description logics, with first order intuitionistic logic and with well-known intuitionistic multi-modal logics. We conclude by presenting an application for a different constructive semantics for KALC in the context of Semantic Web services composition