The Shape of $\mathcal{EL}$ Proofs: A Tale of Three Calculi (Extended Version)

TL;DR

This paper compares three consequence-based calculi for reasoning in the $\

Contribution

It introduces a method to analyze and compare the proof shapes generated by different $\

Findings

Different calculi produce proofs with distinct shapes and complexities.

The translation into existential rules enables detailed proof analysis.

The approach facilitates understanding of proof structure in $\

Abstract

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.