Explaining an answer to a Datalog query is an essential task towards Explainable AI, especially nowadays where Datalog plays a critical role in the development of ontology-based applications. A well-established approach for explaining a query answer is the so-called why-provenance, which essentially collects all the subsets of the input database that can be used to obtain that answer via some derivation process, typically represented as a proof tree. It is well known, however, that computing the why-provenance for Datalog queries is computationally expensive, and thus, very few attempts can be found in the literature. The goal of this work is to demonstrate how off-the-shelf SAT solvers can be exploited towards an efficient computation of the why-provenance for Datalog queries. Interestingly, our SAT-based approach allows us to build the why-provenance in an incremental fashion, that is, one explanation at a time, which is much more useful in a practical context than the one-shot computation of the whole set of explanations as done by existing approaches.
Computing the Why-Provenance for Datalog Queries via SAT Solvers / M. Calautti, E. Livshits, A. Pieris, M. Schneider (PROCEEDINGS OF THE ... AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE). - In: AAAI 2024 Proceedings / [a cura di] M. Wooldridge, J. Dy, S. Natarajan. - [s.l] : Association for the Advancement of Artificial Intelligence, 2024. - ISBN 978-1-57735-887-9. - pp. 10459-10466 (( Intervento presentato al 38. convegno AAAI Conference on Artificial Intelligence tenutosi a Vancouver nel 2024 [10.1609/aaai.v38i9.28914].
Computing the Why-Provenance for Datalog Queries via SAT Solvers
M. Calautti;
2024
Abstract
Explaining an answer to a Datalog query is an essential task towards Explainable AI, especially nowadays where Datalog plays a critical role in the development of ontology-based applications. A well-established approach for explaining a query answer is the so-called why-provenance, which essentially collects all the subsets of the input database that can be used to obtain that answer via some derivation process, typically represented as a proof tree. It is well known, however, that computing the why-provenance for Datalog queries is computationally expensive, and thus, very few attempts can be found in the literature. The goal of this work is to demonstrate how off-the-shelf SAT solvers can be exploited towards an efficient computation of the why-provenance for Datalog queries. Interestingly, our SAT-based approach allows us to build the why-provenance in an incremental fashion, that is, one explanation at a time, which is much more useful in a practical context than the one-shot computation of the whole set of explanations as done by existing approaches.File | Dimensione | Formato | |
---|---|---|---|
C30 (AAAI 2024).pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
656.3 kB
Formato
Adobe PDF
|
656.3 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.