Detecting Non-Existence of Finite Universal Models for Existential Rules

From International Center for Computational Logic

Detecting Non-Existence of Finite Universal Models for Existential Rules

Talk by Lukas Gerlach
For reasoning over ontologies, (finite) universal models play an important role in tasks like conjunctive query answering, which is undecidable. The (restricted) chase is a sound and complete algorithm for computing (finite) universal models of ontologies featuring existential rules. Termination of the chase is undecidable and various sufficient conditions for termination and non-termination have been studied. If the chase terminates, we obtain a finite universal model. However, if the chase does not terminate, a finite universal model may still exist. In recent work, it has been shown that for certain ontologies for which the chase terminates, there exists a chase sequence that yields a universal model that is a core and therefore is the smallest universal model for the given rule set up to isomorphism. We extend this result to non-terminating chase sequences. By that, we are able to introduce a sufficient condition for the existence of an infinite universal model that is a core which in turn implies that no finite universal model exists.

Note that this talk acts as a colloquium/examination for the module INF-PM-FPG. It will take place online via BigBlueButton. To access the room, take one of the following links:

with ZIH-login:

https://selfservice.zih.tu-dresden.de/l/link.php?m=86971&p=30896df0

without ZIH-login:

https://selfservice.zih.tu-dresden.de/link.php?m=86971&p=83001746