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 based on the Kripke semantics for Intuitionistic Logic. Moreover we give a tableau calculus and we show that it is sound, complete and terminating.
A decidable constructive description logic / L. Bozzato, M. Ferrari, C. Fiorentini, G. Fiorino. - In: Logics in artificial intelligence / [a cura di] T. Janhunen, I. Niemelä. - Berlin : Springer, 2010. - ISBN 9783642156748. - pp. 51-63 (( Intervento presentato al 12. convegno European Conference on Logics in Artificial Intelligence tenutosi a Helsinki nel 2010.
A decidable constructive description logic
C. Fiorentini;
2010
Abstract
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 based on the Kripke semantics for Intuitionistic Logic. Moreover we give a tableau calculus and we show that it is sound, complete and terminating.
| File | Dimensione | Formato | |
|---|---|---|---|
|
2010_jelia.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
270.65 kB
Formato
Adobe PDF
|
270.65 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
