Don’t Repeat Yourself: Termination of the Skolem Chase on Disjunctive Existential Rules
From International Center for Computational Logic
Don’t Repeat Yourself: Termination of the Skolem Chase on Disjunctive Existential Rules
project thesis by Lukas Gerlach
- Supervisor Markus Krötzsch, David Carral
- Wissensbasierte Systeme
- 1 April 2020 – 30 September 2020
- Download
Disjunctive Existential Rules are a fragment of first order logic that is already expressive enough to capture many description logics. Conjunctive Query answering is an important reasoning task over such rules. Although this problem is undecidable, different variants of the chase provide sound and complete algorithms that can be used as a reasoning basis. Since it is undecidable if these algorithms terminate for a specific rule set, sufficient conditions for termination, called acyclicity notions, are introduced. We develop Disjunctive Model Faithful Acyclicity (DMFA) as a novel acyclicity notion for the disjunctive skolem chase variant by using ideas from Model Faithful Acyclicity (MFA) for the non-disjunctive skolem chase and Restricted Model Faithful Acyclicity (RMFA) for the restricted chase. Our research shows that our notion captures MFA and is able give a better approximation for termination on disjunctive existential rules. Acyclicity notions for the restricted chase like RMFA still capture DMFA but these notions are not sound for the disjunctive skolem chase. Our results encourage the use of the disjunctive skolem chase in practical applications, which is implementable using well optimized ASP solvers.
Slides available at: https://gitlab.com/m0nstR/defence-grosser-beleg/-/blob/master/build/defence-lukas-gerlach.pdf
