One of the main concerns of constructive semantics is to provide a computational interpretation for the proofs of a given logic. In this paper we introduce a constructive semantics for the basic description logic ALC in the spirit of the BHK interpretation. We prove that such a semantics provides an interpretation of ALC formulas consistent with the classical one and we show how, according to such a semantics, proofs of a suitable natural deduction calculus for ALC support a proofs-as- programs paradigm.
A constructive semantics for ALC / L. Bozzato, M. Ferrari, C. Fiorentini, G. Fiorino - In: Proceedings of the 20th International workshop on description logics, DL'07 : June 8-10, 2007, Free University of Bozen-Bolzano, Brixen/Bressanone, Italy / [a cura di] D. Calvanese ... [et al.]. - Bolzano : Bozen-Bolzano University Press, 2007. - ISBN 9788860460085. - pp. 219-226 (( Intervento presentato al 20. convegno Workshop on Description Logic tenutosi a Bressanone nel 2007.
A constructive semantics for ALC
C. Fiorentini;
2007
Abstract
One of the main concerns of constructive semantics is to provide a computational interpretation for the proofs of a given logic. In this paper we introduce a constructive semantics for the basic description logic ALC in the spirit of the BHK interpretation. We prove that such a semantics provides an interpretation of ALC formulas consistent with the classical one and we show how, according to such a semantics, proofs of a suitable natural deduction calculus for ALC support a proofs-as- programs paradigm.
| File | Dimensione | Formato | |
|---|---|---|---|
|
2007_dl.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
216.38 kB
Formato
Adobe PDF
|
216.38 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
