Statusvortrag im Rahmen des Promotionsver­fahrens von Lukas Gerlach

Title: „Recurring Problems: Decidability, Sufficient Conditions and Formal Verification for Chase Termination”

Abstract: The chase is a sound and complete but possibly non-terminating procedure for query answering over ontologies that feature existential rules (aka. tuple-generating dependencies), a highly expressive knowledge representation language. Termination of the procedure is undecidable in the general case but for some language fragments the problem becomes decidable. A fruitful line of research has established many sufficient conditions for termination and non-termination of the chase. Despite these efforts, our collective understanding seems to be misled by deceptive intuitions at times. In my status talk, I will summarize my involvement in recent contributions to the research area of chase termination, focusing mainly on insights into (un)decidability, improved sufficient conditions for (non-)termination, and an attempt at formally verifying the latter while introducing additional generalization.

Betreuer: Prof. Markus Krötzsch
Fachreferent: Prof. Sebastian Rudolph