An ExpTime Procedure for Description Logic $\mathcal{ALCQI}$ (Draft)
Yu Ding
TL;DR
This paper presents a worst-case exponential time tableau-based decision procedure for checking the satisfiability of the description logic $ ext{ALCQI}$ with respect to general axioms, advancing reasoning methods in this logic.
Contribution
It introduces a new ExpTime tableau-based decision procedure for $ ext{ALCQI}$, handling general axioms, which was not previously available.
Findings
The procedure operates within exponential time in the worst case.
It effectively handles the satisfiability problem for $ ext{ALCQI}$ with axioms.
The approach improves reasoning capabilities in expressive description logics.
Abstract
A worst-case ExpTime tableau-based decision procedure is outlined for the satisfiability problem in w.r.t. general axioms.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSemantic Web and Ontologies · Logic, Reasoning, and Knowledge · Natural Language Processing Techniques