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 fulfills 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 / M. Ferrari, C. Fiorentini, G. Fiorino. - In: JOURNAL OF AUTOMATED REASONING. - ISSN 0168-7433. - 44:4(2010 Apr), pp. 371-399. [10.1007/s10817-009-9160-7]
BCDL : Basic Constructive Description Logic
C. Fiorentini;
2010
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 fulfills the proofs-as-programs paradigm. Finally, we discuss the role of generators, the main element distinguishing our formalisation from the usual ones.
| File | Dimensione | Formato | |
|---|---|---|---|
|
jar2010.pdf
accesso aperto
Tipologia:
Pre-print (manoscritto inviato all'editore)
Dimensione
536.1 kB
Formato
Adobe PDF
|
536.1 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
