Advertisement
Published in:
12-06-2018
A PSpace Algorithm for Acyclic Epistemic DL \(\mathcal {ALCS}5_m\)
Published in: Journal of Automated Reasoning | Issue 3/2019
Log inActivate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Abstract
We study the description language \(\mathcal {ALCS}5_m\), a variant of \(\mathcal {ALCK}_m\) and \(\mathcal {ALCS}4_m\). It augments \(\mathcal {ALC}\) by allowing multi-modal epistemic operators over concept and role expressions. The epistemic operators are interpreted in modal logic \(\mathbf {S}5_m\). By examining design issues of the tableau algorithm specific for \(\mathcal {ALCS}5_m\), different from those for \(\mathcal {ALCK}_m\) and \(\mathcal {ALCS}4_m\), we provide a sound and complete tableau algorithm for deciding the satisfiability of an \(\mathcal {ALCS}5_m\) knowledge base with an acyclic TBox, and further show how it can be implemented in PSpace.