Semiring Provenance for Lightweight Description Logics

TL;DR

This work develops a unified semiring provenance framework for description logics, extending the relational provenance paradigm to annotated ontologies in the lightweight ELHI family. It defines annotated-ontology semantics, canonical models, and provenance computations for axioms and queries, and studies how these notions align with fuzzy, possibilistic, and access-control interpretations under various semiring properties. The paper presents a completion-based approach to compute provenance for annotated assertions and BCQs, analyzes complexity across fragments like ${ m ELHI}^{n}_ot$ and ${ m ELHI}^{n,-}_ot$, and links the DL provenance to Datalog and relational semantics. It also explores specialized semirings (Why[X], PosBool[X], Lin[X]) and their connections to axiom pinpointing, lean kernels, and provenance-inspired explanations, offering both theoretical insights and algorithmic procedures for practical provenance management in ontology-based reasoning. The results illuminate when provenance behaves consistently with database provenance and how to leverage canonical models for efficient reasoning, with implications for explainability and justification in Semantic Web applications. Overall, the framework enables traceable, semantically meaningful explanations of DL entailments and query answers across a spectrum of annotation regimes while preserving favorable computational properties in targeted fragments.

Abstract

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 semiring and these annotations are propagated to the ontology consequences in a way that reflects how they are derived. We define a provenance semantics for a language that encompasses several lightweight description logics and show its relationships with semantics that have been defined for ontologies annotated with a specific kind of annotation (such as fuzzy degrees). We show that under some restrictions on the semiring, the semantics satisfies desirable properties (such as extending the semiring provenance defined for databases). We then focus on the well-known why-provenance, for which we study the complexity of problems related to the provenance of an assertion or a conjunctive query answer. Finally, we consider two more restricted cases which correspond to the so-called positive Boolean provenance and lineage in the database setting. For these cases, we exhibit relationships with well-known notions related to explanations in description logics and complete our complexity analysis. As a side contribution, we provide conditions on an $\mathcal{ELHI}_\bot$ ontology that guarantee tractable reasoning.

Figures (3)

• Figure 1: A hierarchy of provenance semirings GreenT17. $\mathbb{K}_1\rightarrow\mathbb{K}_2$ means that there exists a surjective semiring homomorphism from $\mathbb{K}_1$ to $\mathbb{K}_2$.
• Figure 2: Modified completion rules for the case where $\mathcal{O}\xspace$ belongs to ${\cal E\!LHI}\xspace^{n,-}_\bot$. Note that in $\mathsf{CR}^T_{3}$ and $\mathsf{CR}^T_{4}$, the conjunction $B_1\sqcap\dots\sqcap B_k\sqcap B'_1\sqcap\dots\sqcap B'_{k'}$ contains at most two concept names since $k+k'\leq 2$.
• Figure 3: Construction of the canonical model of a satisfiable $\sf{Why}[{\sf X}\xspace]$-annotated ${\cal E\!LHI}\xspace^n_\bot$ ontology in normal form. $A,A_1,A_2\in{\sf N_C}\xspace\cup\{\top\}$, $B\in{\sf N_C}\xspace$, and $R,S\in {\sf N_R}\xspace$ (recall that RIs and GCIs of $\mathcal{O}\xspace$ are of these forms, except negative RIs and GCIs with $\bot$ as right-hand side, which are not needed since $\mathcal{O}\xspace$ is satisfiable). Since we assume that axioms of $\mathcal{O}\xspace$ are annotated with variables or $1$, all annotations are monomials.

Theorems & Definitions (159)

• Definition 2.1: ${\cal E\!LHI}\xspace^{n,-}_\bot$
• Theorem 2.2
• Remark 2.3
• Remark 3.1
• Remark 3.2: Unsatisfiable concept/role
• Definition 3.3
• Lemma 3.3
• proof
• Proposition 3.4
• proof