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. © 2009 Springer Science+Business Media B.V.
Citazione: | Ferrari, M., Fiorentini, C., & Fiorino, G.G. (2010). BCDL: Basic Constructive Description Logic. JOURNAL OF AUTOMATED REASONING, 44(4), 371-399. |
Tipo: | Articolo in rivista - Articolo scientifico |
Carattere della pubblicazione: | Scientifica |
Titolo: | BCDL: Basic Constructive Description Logic |
Autori: | Ferrari, M; Fiorentini, C; Fiorino, GG |
Autori: | |
Data di pubblicazione: | 2010 |
Lingua: | English |
Rivista: | JOURNAL OF AUTOMATED REASONING |
Digital Object Identifier (DOI): | 10.1007/s10817-009-9160-7 |
Appare nelle tipologie: | 01 - Articolo su rivista |
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.