In this paper we present BCDL, a description logic based on information terms semantics, which allows a constructive interpretation of ALC formulas. In the paper we describe the information terms semantics, we define a natural deduction calculus for BCDL and we show it is sound and complete. As a first application of proof-theoretical properties of the calculus, we show how it fulfils the proofs-as-programs paradigm. Finally, we discuss the role of generators, the main element distinguishing our formalisation from the usual ones.
BCDL: Basic Constructive Description Logic
FERRARI, MAURO;FIORENTINI, CAMILLO;FIORINO, GUIDO
2010-01-01
Abstract
In this paper we present BCDL, a description logic based on information terms semantics, which allows a constructive interpretation of ALC formulas. In the paper we describe the information terms semantics, we define a natural deduction calculus for BCDL and we show it is sound and complete. As a first application of proof-theoretical properties of the calculus, we show how it fulfils the proofs-as-programs paradigm. Finally, we discuss the role of generators, the main element distinguishing our formalisation from the usual ones.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
bcdl-jar.pdf
non disponibili
Tipologia:
Documento in Post-print
Licenza:
DRM non definito
Dimensione
536.1 kB
Formato
Adobe PDF
|
536.1 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.
