The Shape of $\mathcal{EL}$ Proofs: A Tale of Three Calculi (Extended Version)
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909710865661952 |
|---|---|
| author | Alrabbaa, Christian Borgwardt, Stefan Herrmann, Philipp Krötzsch, Markus |
| author_facet | Alrabbaa, Christian Borgwardt, Stefan Herrmann, Philipp Krötzsch, Markus |
| contents | Consequence-based reasoning can be used to construct proofs that explain entailments of description logic (DL) ontologies. In the literature, one can find multiple consequence-based calculi for reasoning in the $\mathcal{EL}$ family of DLs, each of which gives rise to proofs of different shapes. Here, we study three such calculi and the proofs they produce on a benchmark based on the OWL Reasoner Evaluation. The calculi are implemented using a translation into existential rules with stratified negation, which had already been demonstrated to be effective for the calculus of the ELK reasoner. We then use the rule engine NEMO to evaluate the rules and obtain traces of the rule execution. After translating these traces back into DL proofs, we compare them on several metrics that reflect different aspects of their complexity. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_21851 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The Shape of $\mathcal{EL}$ Proofs: A Tale of Three Calculi (Extended Version) Alrabbaa, Christian Borgwardt, Stefan Herrmann, Philipp Krötzsch, Markus Logic in Computer Science Consequence-based reasoning can be used to construct proofs that explain entailments of description logic (DL) ontologies. In the literature, one can find multiple consequence-based calculi for reasoning in the $\mathcal{EL}$ family of DLs, each of which gives rise to proofs of different shapes. Here, we study three such calculi and the proofs they produce on a benchmark based on the OWL Reasoner Evaluation. The calculi are implemented using a translation into existential rules with stratified negation, which had already been demonstrated to be effective for the calculus of the ELK reasoner. We then use the rule engine NEMO to evaluate the rules and obtain traces of the rule execution. After translating these traces back into DL proofs, we compare them on several metrics that reflect different aspects of their complexity. |
| title | The Shape of $\mathcal{EL}$ Proofs: A Tale of Three Calculi (Extended Version) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2507.21851 |