A Constructive Semantics for ALC

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.

• Type: Conference
• Year: 2007
• Where: DLOG
• Authors: Loris Bozzato, Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
• Keywords: ALC Formulas, Automated Reasoning, Constructive Semantics, Description Logic Alc, DLOG 2007