A constructive semantics for ALC
Loris Bozzato, Mauro Ferrari, Camillo Fiorentini, Guido Fiorino · BOA (University of Milano-Bicocca) · 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-asprograms paradigm. 1