KALC: a constructive semantics for ALC
In this article 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.
VILLA Paola;
2011-07-19
Lavoisier
JRC62439
1166-3081,
http://jancl.e-revues.com/acceuil.jsp,
https://publications.jrc.ec.europa.eu/repository/handle/JRC62439,
10.3166/JANCL.21.233–254,
Additional supporting files
| File name | Description | File type | |
|---|
