Name
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. |
Year | Venue | Keywords |
|---|---|---|
2007 | Description Logics | description logic,natural deduction,programming paradigm |
Field | DocType | Citations |
Intuitionistic logic,Horn clause,Programming language,Natural deduction,Constructive,Computer science,Description logic,Philosophy of logic,Logic programming,Semantics | Conference | 8 |
PageRank | References | Authors |
0.66 | 7 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Loris Bozzato | 1 | 54 | 16.23 |
| Mauro Ferrari | 2 | 93 | 16.05 |
| Camillo Fiorentini | 3 | 121 | 21.00 |
| Guido Fiorino | 4 | 97 | 12.71 |