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.
A decidable constructive description logic
Bozzato L.;FERRARI, MAURO;FIORENTINI, CAMILLO;FIORINO, GUIDO
2010-01-01
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 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.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
jelia2010.pdf
non disponibili
Tipologia:
Documento in Post-print
Licenza:
DRM non definito
Dimensione
270.65 kB
Formato
Adobe PDF
|
270.65 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
