IDSIA Seminars

 

Dr Paola Villa - KALC: a constructive semantics for ALC

 

In this talk we firstly present a Kripke semantics for the description logic ALC which is directly inspired by the semantics for Intuitionistic logic. Moreover, we discuss why a direct translation of this kind of semantics is not adequate in the description logic context and propose a constructive semantics that differs from the previous one by the fact that we impose a condition on the partial order. We also present a tableau calculus which is sound and complete with respect to our semantics. As an application of the calculus we prove that this semantics meets the disjunction property, a key criterion used in assessing whether a logic is constructive.

 

20 aprile 2010 11:30

 
 
Made on a Mac

next >

< prev