Consequence-based Reasoning for Description Logics with Disjunction, Inverse Roles, Number Restrictions, and Nominals
We present a consequence-based calculus for concept subsumption and classification in the description logic ALCHOIQ, which extends ALC with role hierarchies, inverse roles, number restrictions, and nominals. By using standard transformations, our calculus extends to SROIQ, which covers all of OWL 2 DL except for datatypes. A key feature of our calculus is its pay-as-you-go behaviour: unlike existing algorithms, our calculus is worst-case optimal for all the well-known proper fragments of ALCHOIQ, albeit not for the full logic.
Code (0)
등록된 구현이 없습니다.
Tasks
AllGeneral ClassificationSimilar Papers 제목 키워드 기반
Extending Consequence-Based Reasoning to SRIQ
Consequence-based calculi are a family of reasoning algorithms for description logics (DLs), and they combine hypertableau and resolution in a way that often achieves excellent performance in practice. Up to now, however…
Towards Statistical Reasoning in Description Logics over Finite Domains (Full Version)
We present a probabilistic extension of the description logic $\mathcal{ALC}$ for reasoning about statistical knowledge. We consider conditional statements over proportions of the domain and are interested in the probabi…
A Primer for Preferential Non-Monotonic Propositional Team Logics
This paper considers KLM-style preferential non-monotonic reasoning in the setting of propositional team semantics. We show that team-based propositional logics naturally give rise to cumulative non-monotonic entailment …
Semiring Provenance for Lightweight Description Logics
We investigate semiring provenance--a successful framework originally defined in the relational database setting--for description logics. In this context, the ontology axioms are annotated with elements of a commutative …
Evonne: Interactive Proof Visualization for Description Logics (System Description) -- Extended Version
Explanations for description logic (DL) entailments provide important support for the maintenance of large ontologies. The "justifications" usually employed for this purpose in ontology editors pinpoint the parts of the …