标题： 一种单一方法来判定线性存在规则上的Chase终止性 显示英文标题

标题： A Single Approach to Decide Chase Termination on Linear Existential Rules

摘要： 存在性规则，长期以来在数据库理论中被称为元组生成依赖，过去十年来作为表示基于本体的查询回答上下文中本体知识的强大形式得到了深入研究。 一个知识库由包含不完整数据的实例和一组存在性规则组成，查询的答案是从知识库中逻辑推导出来的。 这再次引起了对基本追逐工具及其在文献中提出的不同变体的关注。 众所周知，给定一个追逐变体和一组存在性规则，确定追逐在任何实例上是否会停止的问题是不可判定的。 因此，一个关键问题是，对于已知的存在性规则子类，它是否变得可判定。 在这项工作中，我们考虑线性存在性规则，这是一个简单但重要的存在性规则子类，它推广了包含依赖关系。 我们证明了对于三种主要的追逐变体（即半盲目追逐、受限追逐和核心追逐），在线性规则上的所有实例追逐终止问题具有可判定性。 为了获得这些结果，我们引入了一种基于所谓推导树和单一禁止模式的新方法。 除了统一方法和新证明的理论兴趣外，我们提供了关于受限追逐终止的第一个积极的可判定性结果，证明了在线性存在性规则上，该问题的两种版本的追逐终止都是可判定的：每个公平的追逐序列是否会终止？是否存在某个公平的追逐序列会终止？ 显示英文摘要

摘要： Existential rules, long known as tuple-generating dependencies in database theory, have been intensively studied in the last decade as a powerful formalism to represent ontological knowledge in the context of ontology-based query answering. A knowledge base is then composed of an instance that contains incomplete data and a set of existential rules, and answers to queries are logically entailed from the knowledge base. This brought again to light the fundamental chase tool, and its different variants that have been proposed in the literature. It is well-known that the problem of determining, given a chase variant and a set of existential rules, whether the chase will halt on any instance, is undecidable. Hence, a crucial issue is whether it becomes decidable for known subclasses of existential rules. In this work, we consider linear existential rules, a simple yet important subclass of existential rules that generalizes inclusion dependencies. We show the decidability of the all instance chase termination problem on linear rules for three main chase variants, namely semi-oblivious, restricted and core chase. To obtain these results, we introduce a novel approach based on so-called derivation trees and a single notion of forbidden pattern. Besides the theoretical interest of a unified approach and new proofs, we provide the first positive decidability results concerning the termination of the restricted chase, proving that chase termination on linear existential rules is decidable for both versions of the problem: Does every fair chase sequence terminate? Does some fair chase sequence terminate?