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
Bozzato, L., Ferrari, M., Fiorentini, C., Fiorino, G. (2007). A constructive semantics for ALC. In Proceedings of the 2007 International Workshop on Description Logics (DL2007).
A constructive semantics for ALC
FIORINO, GUIDO GIUSEPPE
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 | |
|---|---|---|---|
|
paper_45.pdf
accesso aperto
Dimensione
197.33 kB
Formato
Adobe PDF
|
197.33 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
