Return to Seminars

September 16, 2021, 4 PM: Maël Abily, Lucas Larroque (GraphiK)

Le 16 septembre, à 16h00, Salle 3.124. Maël et Lucas présenteront le travail qu’ils ont réalisé lors de leur stage dans notre équipe.

Join us on Zoom Meeting

Presentation 1

Présentateur : Maël Abily

Title: Implementing the Core Chase for Horn-ALCH

Abstract : The computation of universal models can be used to solve query entailment: a query υ follows from some first-order logic (FOL) theory T if and only if some universal model of T entails υ. Arguably, the best algorithm to compute universal models is the core chase, which is guaranteed to terminate on an input theory T if T admits a finite universal model at all. Unfortunately, due to the complexity of this theoretical procedure, no practical implementations have been developed yet. In this proposal, I discuss an approach to develop an implementation of the core chase for the Description Logic ALCH, which is a decidable fragment of FOL widely used in the context of ontological reasoning.


Presentation 2

Présentateur : Lucas Larroque

Title: Normalization Procedures for Existential Rules that Preserve Chase Termination

Abstract: Recent work on existential rule consider existential rules with certain properties and provide procedures to ensure those properties on existential rule sets. A normalization procedures is a function that transforms any rule set into another one that has the same logical consequences and has the wanted property. The chase is an algorithm that, from a knowledge base, produces a universal model. Although it is sound and complete, it may not terminate. The impact of those normalization procedures on chase termination has not been studied. Given a terminating rule set, does the chase terminate on the normalized rule set? We answer this question for several chase variants, namely the oblivious chase, the semi-oblivious chase, the restricted chase, the Datalog-first restricted chase and the equivalent chase, and for several normalization procedures, one ensuring that rules only have a single piece in the head (with a piece being the minimal unit of information contained in a rule), and the two other that rules only have one atom in the head. To do so, we introduce the notion of universal-conservative extension to characterize normalization procedures that preserve the termination of the equivalent chase, and we use different proof techniques adapted to each chase variant.

Permanent link to this article: