Università degli Studi dell'Insubria Insubria Space

InsubriaSPACE - Thesis PhD Repository >
Insubria Thesis Repository >
01 - Tesi di dottorato >

Please use this identifier to cite or link to this item: http://hdl.handle.net/10277/272

Authors: Bozzato, Loris
Internal Tutor: FERRARI, MAURO
Title: Kripke semantics and tableau procedures for constructive description logics.
Abstract: 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
Keywords: description logics, constructive logics, proof theory
Issue Date: 2011
Language: en
Doctoral course: Informatica
Academic cycle: 23
Publisher: Università degli Studi dell'Insubria
Citation: Bozzato, L.Kripke semantics and tableau procedures for constructive description logics. (Doctoral Thesis, Università degli Studi dell'Insubria, 2011).

Files in This Item:

File Description SizeFormatVisibility
Phd_thesis_bozzato_completa.pdftesto completo tesi587,16 kBAdobe PDFView/Open

Items in InsubriaSPACE are protected by copyright, with all rights reserved, unless otherwise indicated.

Share this record




Stumble it!



  ICT Support, development & maintenance are provided by the AePIC team @ CILEA. Powered on DSpace Software.  Feedback