Generalized Satisfiability for the Description Logic ALC
Arne Meier, Thomas Schneider
TL;DR
This paper classifies the computational complexity of concept satisfiability in all Boolean and quantifier fragments of ALC description logic with general axioms, extending understanding beyond known fragments.
Contribution
It provides a comprehensive complexity classification for all Boolean and quantifier fragments of ALC with general axioms, covering previously uncharacterized cases.
Findings
Complexity classifications for all ALC fragments with axioms
Identification of tractable and intractable cases
Extension of known results to broader fragments
Abstract
The standard reasoning problem, concept satisfiability, in the basic description logic ALC is PSPACE-complete, and it is EXPTIME-complete in the presence of unrestricted axioms. Several fragments of ALC, notably logics in the FL, EL, and DL-Lite families, have an easier satisfiability problem; sometimes it is even tractable. We classify the complexity of the standard satisfiability problems for all possible Boolean and quantifier fragments of ALC in the presence of 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
TopicsFormal Methods in Verification · Logic, Reasoning, and Knowledge · Semantic Web and Ontologies