Characterizing Boundedness in Chase Variants

Autor: Marie-Laure Mugnier, Michel Leclère, Stathis Delivorias, Federico Ulliana
Přispěvatelé: Graphs for Inferences on Knowledge (GRAPHIK), Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier (LIRMM), Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM)-Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM)-Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), University of Montpellier, LIRMM (UM, CNRS), Université de Montpellier (UM)-Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM)-Centre National de la Recherche Scientifique (CNRS)-Inria Sophia Antipolis - Méditerranée (CRISAM)
Rok vydání: 2020
Předmět:
FOS: Computer and information sciences
Computer Science - Logic in Computer Science
Chase
Computer Science - Artificial Intelligence
Computer science
Context (language use)
0102 computer and information sciences
02 engineering and technology
01 natural sciences
[INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI]
Theoretical Computer Science
Set (abstract data type)
Integer
Fragment (logic)
Artificial Intelligence
0202 electrical engineering
electronic engineering
information engineering

Existential rules
Discrete mathematics
Boundedness
[INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB]
TGD
Logic in Computer Science (cs.LO)
Decidability
Undecidable problem
Artificial Intelligence (cs.AI)
Computational Theory and Mathematics
010201 computation theory & mathematics
Hardware and Architecture
Bounded function
020201 artificial intelligence & image processing
Software
Zdroj: Theory and Practice of Logic Programming
Theory and Practice of Logic Programming, Cambridge University Press (CUP), 2021, 21 (1), pp.51-79. ⟨10.1017/S1471068420000083⟩
Theory and Practice of Logic Programming, 2021, 21 (1), pp.51-79. ⟨10.1017/S1471068420000083⟩
ISSN: 1475-3081
1471-0684
DOI: 10.1017/s1471068420000083
Popis: Existential rules are a positive fragment of first-order logic that generalizes function-free Horn rules by allowing existentially quantified variables in rule heads. This family of languages has recently attracted significant interest in the context of ontology-mediated query answering. Forward chaining, also known as the chase, is a fundamental tool for computing universal models of knowledge bases, which consist of existential rules and facts. Several chase variants have been defined, which differ on the way they handle redundancies. A set of existential rules is bounded if it ensures the existence of a bound on the depth of the chase, independently from any set of facts. Deciding if a set of rules is bounded is an undecidable problem for all chase variants. Nevertheless, when computing universal models, knowing that a set of rules is bounded for some chase variant does not help much in practice if the bound remains unknown or even very large. Hence, we investigate the decidability of the k-boundedness problem, which asks whether the depth of the chase for a given set of rules is bounded by an integer k. We identify a general property which, when satisfied by a chase variant, leads to the decidability of k-boundedness. We then show that the main chase variants satisfy this property, namely the oblivious, semi-oblivious (aka Skolem), and restricted chase, as well as their breadth-first versions. This paper is under consideration for publication in Theory and Practice of Logic Programming.
Comment: Under consideration for publication in Theory and Practice of Logic Programming
Databáze: OpenAIRE