335 views
<font size="+3">Decidable Fragments of Horn First-Order Logic</font> <font size="+2">Seminar Organised by the Action Transverse Logique at the LIRMM</font> In this seminar, we present recent results about Existential Rules, an undecidable Horn fragment of first-order logic that is widely used in ontological modelling. Namely, we discuss the main approaches devised to retrieve decidability as well as efficient implementations to solve complex reasoning tasks. <a href="#0" data-toggle="collapse" data-target="#whenwhere"><font size="+1">1. When and Where</font></a> <div id="whenwhere" class="collapse"> <ul> <li>This is a one-day event, which will take place on the 17th of November (Wednesday).</li> <li>The talks will take place in the large seminar room in <a href="https://www.google.com/maps/place/LIRMM+-+Laboratoire+d'informatique,+de+robotique+et+de+micro%C3%A9lectronique+de+Montpellier/@43.6371811,3.8406428,18z/data=!4m8!1m2!2m1!1sB%C3%A2timent+4+-+161,+rue+Ada+34095+Montpellier+cedex+4!3m4!1s0x12b6aeb95b72e417:0x66d6d879ec0770fa!8m2!3d43.6368731!4d3.8403458">Building 4 of the LIRMM</a>.</li> <li>If you want to join us for lunch, which will take place in <a href="https://www.google.com/maps/place/Inria+Montpellier+-+Building+5/@43.6370781,3.8395086,17z/data=!4m8!1m2!2m1!1sBatiment+5++Campus+Saint+Priest+860+rue+de+Saint+Priest+34095+Montpellier+cedex+5+%E2%80%93+France!3m4!1s0x12b6afe511ef3247:0x824c926df4fed43f!8m2!3d43.6370781!4d3.8416973" target="_blank" rel="noopener">Building 5 of the LIRMM</a>, please register using the online form under the "5. Registration" section.</li> </ul> <br> </div> <a href="#0" data-toggle="collapse" data-target="#program"><font size="+1">2. Program</font></a> <div id="program" class="collapse"> <a href="#0" data-toggle="collapse" data-target="#carral"> <font size="+1"> <ul> <li>9:30 to 10:15: "Introduction to Existential Rules" by David Carral</li> </ul> </font> </a> <div id="carral" class="collapse"> <ul> <ul> <li><b>Abstract:</b> David Carral will first introduce the syntax and semantics of existential rules. Then, he will show that reasoning over this expressive fragment of first-order logic is undecidable. Finally, he will present two of the main approaches that are used to retrieve decidability. The first one is based on termination of the chase, a bottom-up materialisation procedure that aims to compute universal models. The second one is based on resolution, a backward-chaining algorithm that can be used to rewrite queries so as to incorporate the semantic information in an existential rule theory. </li> <li><b>Bio</b>: David Carral is a local Inria researcher at the GraphIK team at the University of Montpellier. Broadly speaking, he is interested in the study of logical languages (mostly first-order logic, existential rules, and Description Logics) and their theoretical/computational properties. </li> <li><b>Personal Page:</b> https://www-sop.inria.fr/members/David.Carral/ </li> <li><b>Dates in Montpellier:</b> Local researcher</li> </ul> </ul> </div> <a href="#0" data-toggle="collapse" data-target="#thom"> <font size="+1"> <ul> <li>10:15 to 10:45: "Reasoning with Guarded Existential Rules" by Michaël Thomazo</li> </ul> </font> </a> <div id="thom" class="collapse"> <ul> <ul> <li><b>Abstract:</b> TBA </li> <li><b>Bio</b>: Michaël is an Inria researcher at the Valda research team. He is broadly interested in knowledge representation and its interactions with database theory and database systems, often seen through a logical and/or graph based formalism. He started in this field by getting a Ph.D from the University of Montpellier, supervised by J.-F. Baget and M.-L. Mugnier in the Inria team GraphIK. Then, he joined the group of Sebastian Rudolph at TU Dresden and partially funded through an Alexander von Humboldt fellowship. Afterwards, he was recruited in the Oak/Cedar team of Inria Saclay, before joining Valda in April 2018. </li> <li><b>Personal Page:</b> https://www.di.ens.fr/michael.thomazo/ </li> <li><b>Dates in Montpellier:</b> From the 14/11 (Sunday) to the 18/11 (Thursday)</li> </ul> </ul> </div> <font size="+1"> <ul> <li>10:45 to 11:15: Coffee Break</li> </ul> </font> <a href="#0" data-toggle="collapse" data-target="#urbani"> <font size="+1"> <ul> <li>11:15 to 12:00: "Compressing Rule-based Reasoning" by Jacopo Urbani</li> </ul> </font> </a> <div id="urbani" class="collapse"> <ul> <ul> <li><b>Abstract:</b> Rule-based reasoning on large Knowledge Bases (KBs) is a problem that received significant attention from the AI research community. One of the key reasoning tasks is materialization, i.e., the exhaustive derivation of all facts that can be implied by a set of rules. Many approaches have been proposed to improve the performance of materialization. Most of them focus on parallelism as a means to decrease the runtime. This talk will focus instead on a relatively unexplored way to improve the performance, that is via compression. First, I will present VLog, a leading rule-based reasoner that exploits a column-based representation to compress the derivations. This allows VLog to reason more efficiently, both in terms of runtime and memory consumption. Then, I will present more sophisticated forms of compression which further improve the performance of reasoning.</li> <li><b>Bio</b>: Jacopo Urbani is an professor in Computer Science at the Vrije Universiteit Amsterdam (VUA). He is also a guest researcher at the Centrum Wiskunde & Informatica in Amsterdam. He wrote a PhD thesis on distributed reasoning algorithms for very large Knowledge Graphs. The thesis was nominated by the Royal Netherlands Academy of Arts and Sciences as one of the best PhD theses in Computer Science in the country. After spending part of his postdoc in USA (Stanford) and Germany (MPII), he joined the faculty of the VUA. He recently started a research unit on knowledge extraction and inference from large Web corpora which has developed tools that are considered among the state-of-the-art in the respective fields. </li> <li><b>Personal Page:</b> https://www.jacopourbani.it/ </li> <li><b>Dates in Montpellier:</b> From the 16/11 to the 18/11</li> </ul> </ul> </div> <font size="+1"> <ul> <li>12:00 to 13:30: Lunch Break (to register for lunch please use the online form under the "5. Registration" section)</li> </ul> </font> <a href="#0" data-toggle="collapse" data-target="#rudolph"> <font size="+1"> <ul> <li>13:30 to 14:15: "Capturing Homomorphism-Closed Decidable Queries with Existential Rules" by Sebastian Rudolph</li> </ul> </font> </a> <div id="rudolph" class="collapse"> <ul> <ul> <li><b>Abstract:</b> Existential rules are a very popular ontology-mediated query language for which the chase represents a generic computational approach for query answering. It is straightforward that existential rule queries exhibiting chase termination are decidable and can only recognize properties that are preserved under homomorphisms. In this paper, we show the converse: every decidable query that is closed under homomorphism can be expressed by an existential rule set for which the standard chase universally terminates. Membership in this fragment is not decidable, but we show via a diagonalisation argument that this is unavoidable.</li> <li><b>Bio</b>: Sebastian Rudolph is full professor for computational logic and head of the AI Institute at TU Dresden. His scientific interests revolve around artificial intelligence, with a particular focus on logical formalisms and methods for knowledge representation and reasoning, ranging from theoretical foundations (such as semantic and computational properties) to practical deployment (including ontological modeling and interactive knowledge acquisition). In the course of an ongoing ERC Consolidator Grant, his team currently investigates general principles of decidability in logic-based knowledge representation.</li> <li><b>Personal Page:</b> https://iccl.inf.tu-dresden.de/web/Sebastian_Rudolph/en</li> <li><b>Dates in Montpellier:</b> From the 14/11 (Sunday) to the 29/11 (Monday)</li> </ul> </ul> </div> <a href="#0" data-toggle="collapse" data-target="#thomazo2"> <font size="+1"> <ul> <li>14:15 to 15:00: "Answering Counting Queries over Lightweight Ontologies" by Michaël Thomazo</li> </ul> </font> </a> <div id="thomazo2" class="collapse"> <ul> <ul> <li><b>Abstract:</b> Ontology-mediated query answering (OMQA) is a promising approach to data access and integration that has been actively studied in the knowledge representation and database communities for more than a decade. The vast majority of work on OMQA focuses on conjunctive queries, whereas more expressive queries that feature counting or other forms of aggregation remain largely unexplored. I'll introduce a general form of counting query, relate it to previous proposals, and present come complexity results and associated techniques to answer such counting queries. This is joint work with Meghyn Bienvenu and Quentin Manière.</li> <li><b>Bio</b>: Michaël is an Inria researcher at the Valda research team. He is broadly interested in knowledge representation and its interactions with database theory and database systems, often seen through a logical and/or graph based formalism. He started in this field by getting a Ph.D from the University of Montpellier, supervised by J.-F. Baget and M.-L. Mugnier in the Inria team GraphIK. Then, he joined the group of Sebastian Rudolph at TU Dresden and partially funded through an Alexander von Humboldt fellowship. Afterwards, he was recruited in the Oak/Cedar team of Inria Saclay, before joining Valda in April 2018. </li> <li><b>Personal Page:</b> https://www.di.ens.fr/michael.thomazo/</li> <li><b>Dates in Montpellier:</b> From the 14/11 (Sunday) to the 18/11 (Thursday)</li> </ul> </ul> </div> <font size="+1"> <ul> <li>15:00 to 15:30: Coffee Break</li> </ul> </font> <a href="#0" data-toggle="collapse" data-target="#tim"> <font size="+1"> <ul> <li>15:30 to 16:15: "Derivation Graphs, Greediness, and Bounded-treewidth in the Context of Existential Rules" by Timothy Stephen Lyon</li> </ul> </font> </a> <div id="tim" class="collapse"> <ul> <ul> <li><b>Abstract:</b> This talk will discuss decidable classes of existential rules subsumed by the class of bounded-treewidth sets and interrelationships thereof. We will look at classes of existential rules defined on the basis of "derivation graphs," that is, directed acyclic graphs which record how facts are derived from a given knowledge base. Such objects have been used to identify decidable sets of existential rules given that such graphs can be reduced to a forest via certain reduction operations. Moreover, we will look at classes of existential rules that rely on the concept of a "greedy derivation," i.e. derivations where if a rule is applied, then all frontier variables not mapped to terms from the given data set must be mapped to terms provided by a single, previous rule application. We will conclude the talk by mapping out which classes subsume or identify with one another.</li> <li><b>Bio</b>: Tim is a postdoctoral researcher in the Computational Logic group at Technische Universität Dresden. He currently works within the ERC project DeciGUT, and his research interests concern the construction and application of proof systems for fragments of first-order logic, non-classical logics, and modal logics. Prior to joining TU Dresden, he was a PhD student at Technische Universität Wien, where he worked on the TICAMORE (Translating and Discovering Calculi for Modal and Related Logics) project under the supervision of Prof. Agata Ciabattoni.</li> <li><b>Personal Page:</b> https://iccl.inf.tu-dresden.de/web/Tim_Lyon</li> <li><b>Dates in Montpellier:</b> From the 14/11 (Monday) to the 19/11 (Friday)</li> </ul> </ul> </div> <a href="#0" data-toggle="collapse" data-target="#piotr"> <font size="+1"> <ul> <li>16:15 to 17:00: "Existential rules: Intersecting FO-Rewritability and Core Termination" by Piotr Ostropolski-Nalewaja</li> </ul> </font> </a> <div id="piotr" class="collapse"> <ul> <ul> <li><b>Abstract:</b> At the beginning of the talk, we will introduce two essential classes of existential rules that admit decidable query entailment. First - known as FUS or BDD - achieves this by ensuring the existence of the first-order query rewritings. Second - known as FES or the class of rulesets that are Core Terminating - achieves decidability of query entailment by ensuring the existence of finite universal models. Later, we will explore the intersection of those classes in the context of the FUS/FES conjecture. This talk will be based on the joint work with Jerzy Marcinkowski, David Carral, and Sebastian Rudolph.</li> <li><b>Bio</b>: Piotr Ostropolski-Nalewaja recently started working as a postdoc researcher in the group of Prof. Sebastian Rudolph on the ERC project DeciGUT. Before that Piotr was a PhD student at the University of Wrocław, where he was (mostly) focusing on existential rules.</li> <li><b>Personal Page:</b> https://iccl.inf.tu-dresden.de/web/Piotr_Ostropolski-Nalewaja/en</li> <li><b>Dates in Montpellier:</b> From the 14/11 (Sunday) to the 19/11 (Friday)</li> </ul> </ul> </div> <br> </div> <a href="#0" data-toggle="collapse" data-target="#remark-program"><font size="+1">3. Is this seminar for you?</font></a> <div id="remark-program" class="collapse"> The morning sessions of the program are meant to provide you with a general introduction to Existential Rules. If you are familiar with the syntax and semantics of first-order logic, you should be able to fully understand these presentations. In the afternoon, the talks will be a bit more specific/technical. Hence, if you would like to attend the event (and you are not so familiar with the topic at hand), we strongly suggest that you attend the morning sessions. After that, you can probably decide by yourself if you also want to stay for the rest of the day. <br><br> </div> <a href="#0" data-toggle="collapse" data-target="#why"><font size="+1">4. Why should you attend this event?</font></a> <div id="why" class="collapse"> Wondering if you should come? Our impressive list of international speakers may convince you to do so: <ul> <li>Timothy Stephen Lyon; postdoctoral researcher at TU Dresden</li> <li>Piotr Ostropolski-Nalewaja; postdoctoral researcher at TU Dresden</li> <li>Sebastian Rudolph; professor at TU Dresden</li> <li>Michaël Thomazo; Inria researcher at ENS Paris</li> <li>Jacopo Urbani; professor at VU Amsterdam</li> </ul> Besides, in the afternoon, Sebastian Rudolph will present the paper "Capturing Homomorphism-Closed Decidable Queries with Existential Rules", which has been awarded the 2021 Ray Reiter Best Paper Prize. That is, the best paper award at the 18th International Conference on Principles of Knowledge Representation and Reasoning (KR 2021). <br><br> </div> <a href="#0" data-toggle="collapse" data-target="#registration"><font size="+1">5. Registration</font></a> <div id="registration" class="collapse"> We need to keep attendance because of COVID restrictions! Therefore, we ask all participants to register for the event using this <a href="https://docs.google.com/forms/d/e/1FAIpQLSdak3J8J8OYqFOYHAeqfPbCxLgmIQZ9n_O7FIchR60zQkKAhQ/viewform">online form</a>. Also, please indicate in the form if you will be joining us for lunch. <br><br> </div> <a href="#0" data-toggle="collapse" data-target="#contact"><font size="+1">6. Contact</font></a> <div id="contact" class="collapse"> David Carral (david.carral@inria.fr) and Mégane Miquel (megane.miquel@lirmm.fr) <br><br> </div> <a href="#0" data-toggle="collapse" data-target="#acknowledgements"><font size="+1">7. Acknowledgements</font></a> <div id="acknowledgements" class="collapse"> This seminar is organised within the "Action Transverse Logique", which is funded by the <a href="https://www.lirmm.fr/">LIRMM</a>. Additional funds have been provided by the <a href="https://team.inria.fr/graphik/">GraphIK team</a> and the <a href="https://iccl.inf.tu-dresden.de/web/Computational_Logic/en">Chair of Computational Logic</a> at TU Dresden. <br><br> </div>