-
Restricted Chase Termination: You Want More than Fairness
Authors:
David Carral,
Lukas Gerlach,
Lucas Larroque,
Michaël Thomazo
Abstract:
The chase is a fundamental algorithm with ubiquitous uses in database theory. Given a database and a set of existential rules (aka tuple-generating dependencies), it iteratively extends the database to ensure that the rules are satisfied in a most general way. This process may not terminate, and a major problem is to decide whether it does. This problem has been studied for a large number of chase…
▽ More
The chase is a fundamental algorithm with ubiquitous uses in database theory. Given a database and a set of existential rules (aka tuple-generating dependencies), it iteratively extends the database to ensure that the rules are satisfied in a most general way. This process may not terminate, and a major problem is to decide whether it does. This problem has been studied for a large number of chase variants, which differ by the conditions under which a rule is applied to extend the database. Surprisingly, the complexity of the universal termination of the restricted (aka standard) chase is not fully understood. We close this gap by placing universal restricted chase termination in the analytical hierarchy. This higher hardness is due to the fairness condition, and we propose an alternative condition to reduce the hardness of universal termination.
△ Less
Submitted 22 May, 2025;
originally announced May 2025.
-
In silico design and prediction of metastable quaternary phases in Cu-Ni-Si-Cr alloys
Authors:
Ángel Díaz Carral,
Simon Gravelle,
Maria Fyta
Abstract:
Quaternary phases formed in copper alloys are investigated through a combination of quantum-mechanical and classical computer simulations and active machine learning. Focus is given on nickel, silicon, and chromium impurities in a copper matrix. The analysis of the formation enthalpies of candidate quaternary structures leads to the prediction of two novel quaternary phases and the assessment of t…
▽ More
Quaternary phases formed in copper alloys are investigated through a combination of quantum-mechanical and classical computer simulations and active machine learning. Focus is given on nickel, silicon, and chromium impurities in a copper matrix. The analysis of the formation enthalpies of candidate quaternary structures leads to the prediction of two novel quaternary phases and the assessment of their stability. For the predicted two phases, machine learned atomistic potentials are developed using active learning with a quantum-mechanical accuracy. Use of these potentials in atomistic simulations further elucidates the structure, temperature-dependent dynamics, and elastic behavior of the predicted quaternary phases in copper alloys. The combined in silico approach is thus proven highly efficient in both designing materials and elucidating their properties and potential combining different spatiotemporal scales. In the case of alloys, this computational scheme significantly reduces the effort in searching the huge chemical space of possible phases, enhancing the efficiency in synthesizing novel alloys with pre-defined properties.
△ Less
Submitted 23 October, 2024;
originally announced October 2024.
-
Finite Groundings for ASP with Functions: A Journey through Consistency
Authors:
Lukas Gerlach,
David Carral,
Markus Hecher
Abstract:
Answer set programming (ASP) is a logic programming formalism used in various areas of artificial intelligence like combinatorial problem solving and knowledge representation and reasoning. It is known that enhancing ASP with function symbols makes basic reasoning problems highly undecidable. However, even in simple cases, state of the art reasoners, specifically those relying on a ground-and-solv…
▽ More
Answer set programming (ASP) is a logic programming formalism used in various areas of artificial intelligence like combinatorial problem solving and knowledge representation and reasoning. It is known that enhancing ASP with function symbols makes basic reasoning problems highly undecidable. However, even in simple cases, state of the art reasoners, specifically those relying on a ground-and-solve approach, fail to produce a result. Therefore, we reconsider consistency as a basic reasoning problem for ASP. We show reductions that give an intuition for the high level of undecidability. These insights allow for a more fine-grained analysis where we characterize ASP programs as "frugal" and "non-proliferous". For such programs, we are not only able to semi-decide consistency but we also propose a grounding procedure that yields finite groundings on more ASP programs with the concept of "forbidden" facts.
△ Less
Submitted 8 May, 2024;
originally announced May 2024.
-
Do Repeat Yourself: Understanding Sufficient Conditions for Restricted Chase Non-Termination
Authors:
Lukas Gerlach,
David Carral
Abstract:
The disjunctive restricted chase is a sound and complete procedure for solving boolean conjunctive query entailment over knowledge bases of disjunctive existential rules. Alas, this procedure does not always terminate and checking if it does is undecidable. However, we can use acyclicity notions (sufficient conditions that imply termination) to effectively apply the chase in many real-world cases.…
▽ More
The disjunctive restricted chase is a sound and complete procedure for solving boolean conjunctive query entailment over knowledge bases of disjunctive existential rules. Alas, this procedure does not always terminate and checking if it does is undecidable. However, we can use acyclicity notions (sufficient conditions that imply termination) to effectively apply the chase in many real-world cases. To know if these conditions are as general as possible, we can use cyclicity notions (sufficient conditions that imply non-termination). In this paper, we discuss some issues with previously existing cyclicity notions, propose some novel notions for non-termination by dismantling the original idea, and empirically verify the generality of the new criteria.
△ Less
Submitted 22 September, 2023;
originally announced September 2023.
-
Normalisations of Existential Rules: Not so Innocuous!
Authors:
David Carral,
Lucas Larroque,
Marie-Laure Mugnier,
Michaël Thomazo
Abstract:
Existential rules are an expressive knowledge representation language mainly developed to query data. In the literature, they are often supposed to be in some normal form that simplifies technical developments. For instance, a common assumption is that rule heads are atomic, i.e., restricted to a single atom. Such assumptions are considered to be made without loss of generality as long as all sets…
▽ More
Existential rules are an expressive knowledge representation language mainly developed to query data. In the literature, they are often supposed to be in some normal form that simplifies technical developments. For instance, a common assumption is that rule heads are atomic, i.e., restricted to a single atom. Such assumptions are considered to be made without loss of generality as long as all sets of rules can be normalised while preserving entailment. However, an important question is whether the properties that ensure the decidability of reasoning are preserved as well. We provide a systematic study of the impact of these procedures on the different chase variants with respect to chase (non-)termination and FO-rewritability. This also leads us to study open problems related to chase termination of independent interest.
△ Less
Submitted 7 June, 2022;
originally announced June 2022.
-
Deciding Hyperproperties Combined with Functional Specifications
Authors:
Raven Beutner,
David Carral,
Bernd Finkbeiner,
Jana Hofmann,
Markus Krötzsch
Abstract:
We study satisfiability for HyperLTL with a $\forall^*\exists^*$ quantifier prefix, known to be highly undecidable in general. HyperLTL can express system properties that relate multiple traces (so-called hyperproperties), which are often combined with trace properties that specify functional behavior on single traces. Following this conceptual split, we first define several safety and liveness fr…
▽ More
We study satisfiability for HyperLTL with a $\forall^*\exists^*$ quantifier prefix, known to be highly undecidable in general. HyperLTL can express system properties that relate multiple traces (so-called hyperproperties), which are often combined with trace properties that specify functional behavior on single traces. Following this conceptual split, we first define several safety and liveness fragments of $\forall^*\exists^*$ HyperLTL, and characterize the complexity of their (often much easier) satisfiability problem. We then add LTL trace properties as functional specifications. Though (highly) undecidable in many cases, this way of combining "simple" HyperLTL and arbitrary LTL also leads to interesting new decidable fragments. This systematic study of $\forall^*\exists^*$ fragments is complemented by a new (incomplete) algorithm for $\forall\exists^*$-HyperLTL satisfiability.
△ Less
Submitted 30 May, 2022;
originally announced May 2022.
-
Capturing Homomorphism-Closed Decidable Queries with Existential Rules
Authors:
Camille Bourgaux,
David Carral,
Markus Krötzsch,
Sebastian Rudolph,
Michaël Thomazo
Abstract:
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 un…
▽ More
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.
△ Less
Submitted 16 July, 2021;
originally announced July 2021.
-
Materializing Knowledge Bases via Trigger Graphs
Authors:
Efthymia Tsamoura,
David Carral,
Enrico Malizia,
Jacopo Urbani
Abstract:
The chase is a well-established family of algorithms used to materialize Knowledge Bases (KBs), like Knowledge Graphs (KGs), to tackle important tasks like query answering under dependencies or data cleaning. A general problem of chase algorithms is that they might perform redundant computations. To counter this problem, we introduce the notion of Trigger Graphs (TGs), which guide the execution of…
▽ More
The chase is a well-established family of algorithms used to materialize Knowledge Bases (KBs), like Knowledge Graphs (KGs), to tackle important tasks like query answering under dependencies or data cleaning. A general problem of chase algorithms is that they might perform redundant computations. To counter this problem, we introduce the notion of Trigger Graphs (TGs), which guide the execution of the rules avoiding redundant computations. We present the results of an extensive theoretical and empirical study that seeks to answer when and how TGs can be computed and what are the benefits of TGs when applied over real-world KBs. Our results include introducing algorithms that compute (minimal) TGs. We implemented our approach in a new engine, and our experiments show that it can be significantly more efficient than the chase enabling us to materialize KBs with 17B facts in less than 40 min on commodity machines.
△ Less
Submitted 4 February, 2021;
originally announced February 2021.
-
A Journey to the Frontiers of Query Rewritability
Authors:
Piotr Ostropolski-Nalewaja,
Jerzy Marcinkowski,
David Carral,
Sebastian Rudolph
Abstract:
This paper is about (first order) query rewritability in the context of theory-mediated query answering. The starting point of our journey is the FUS/FES conjecture, saying that if a theory is core-terminating (FES) and admits query rewriting (BDD, FUS) then it is uniformly bounded. We show that this conjecture is true for a wide class of "local" BDD theories. Then we ask how non-local can a BDD t…
▽ More
This paper is about (first order) query rewritability in the context of theory-mediated query answering. The starting point of our journey is the FUS/FES conjecture, saying that if a theory is core-terminating (FES) and admits query rewriting (BDD, FUS) then it is uniformly bounded. We show that this conjecture is true for a wide class of "local" BDD theories. Then we ask how non-local can a BDD theory actually be and we discover phenomena which we think are quite counter-intuitive.
△ Less
Submitted 3 May, 2021; v1 submitted 21 December, 2020;
originally announced December 2020.
-
Checking Chase Termination over Ontologies of Existential Rules with Equality
Authors:
David Carral,
Jacopo Urbani
Abstract:
The chase is a sound and complete algorithm for conjunctive query answering over ontologies of existential rules with equality. To enable its effective use, we can apply acyclicity notions; that is, sufficient conditions that guarantee chase termination. Unfortunately, most of these notions have only been defined for existential rule sets without equality. A proposed solution to circumvent this is…
▽ More
The chase is a sound and complete algorithm for conjunctive query answering over ontologies of existential rules with equality. To enable its effective use, we can apply acyclicity notions; that is, sufficient conditions that guarantee chase termination. Unfortunately, most of these notions have only been defined for existential rule sets without equality. A proposed solution to circumvent this issue is to treat equality as an ordinary predicate with an explicit axiomatisation. We empirically show that this solution is not efficient in practice and propose an alternative approach. More precisely, we show that, if the chase terminates for any equality axiomatisation of an ontology, then it terminates for the original ontology (which may contain equality). Therefore, one can apply existing acyclicity notions to check chase termination over an axiomatisation of an ontology and then use the original ontology for reasoning. We show that, in practice, doing so results in a more efficient reasoning procedure. Furthermore, we present equality model-faithful acyclicity, a general acyclicity notion that can be directly applied to ontologies with equality.
△ Less
Submitted 25 November, 2019;
originally announced November 2019.
-
Rule-based OWL Modeling with ROWLTab Protege Plugin
Authors:
Md. Kamruzzaman Sarker,
Adila Krisnadhi,
David Carral,
Pascal Hitzler
Abstract:
It has been argued that it is much easier to convey logical statements using rules rather than OWL (or description logic (DL)) axioms. Based on recent theoretical developments on transformations between rules and DLs, we have developed ROWLTab, a Protege plugin that allows users to enter OWL axioms by way of rules; the plugin then automatically converts these rules into OWL 2 DL axioms if possible…
▽ More
It has been argued that it is much easier to convey logical statements using rules rather than OWL (or description logic (DL)) axioms. Based on recent theoretical developments on transformations between rules and DLs, we have developed ROWLTab, a Protege plugin that allows users to enter OWL axioms by way of rules; the plugin then automatically converts these rules into OWL 2 DL axioms if possible, and prompts the user in case such a conversion is not possible without weakening the semantics of the rule. In this paper, we present ROWLTab, together with a user evaluation of its effectiveness compared to entering axioms using the standard Protege interface. Our evaluation shows that modeling with ROWLTab is much quicker than the standard interface, while at the same time, also less prone to errors for hard modeling tasks.
△ Less
Submitted 30 August, 2018;
originally announced August 2018.
-
Modeling OWL with Rules: The ROWL Protege Plugin
Authors:
Md. Kamruzzaman Sarker,
David Carral,
Adila A. Krisnadhi,
Pascal Hitzler
Abstract:
In our experience, some ontology users find it much easier to convey logical statements using rules rather than OWL (or description logic) axioms. Based on recent theoretical developments on transformations between rules and description logics, we develop ROWL, a Protege plugin that allows users to enter OWL axioms by way of rules; the plugin then automatically converts these rules into OWL DL axi…
▽ More
In our experience, some ontology users find it much easier to convey logical statements using rules rather than OWL (or description logic) axioms. Based on recent theoretical developments on transformations between rules and description logics, we develop ROWL, a Protege plugin that allows users to enter OWL axioms by way of rules; the plugin then automatically converts these rules into OWL DL axioms if possible, and prompts the user in case such a conversion is not possible without weakening the semantics of the rule.
△ Less
Submitted 29 August, 2018;
originally announced August 2018.
-
A Practical Acyclicity Notion for Query Answering over Horn-SRIQ Ontologies
Authors:
David Carral,
Cristina Feier,
Pascal Hitzler
Abstract:
Conjunctive query answering over expressive Horn Description Logic ontologies is a relevant and challenging problem which, in some cases, can be addressed by application of the chase algorithm. In this paper, we define a novel acyclicity notion which provides a sufficient condition for termination of the restricted chase over Horn-SRIQ TBoxes. We show that this notion generalizes most of the exist…
▽ More
Conjunctive query answering over expressive Horn Description Logic ontologies is a relevant and challenging problem which, in some cases, can be addressed by application of the chase algorithm. In this paper, we define a novel acyclicity notion which provides a sufficient condition for termination of the restricted chase over Horn-SRIQ TBoxes. We show that this notion generalizes most of the existing acyclicity conditions (both theoretically and empirically). Furthermore, this new acyclicity notion gives rise to a very efficient reasoning procedure. We provide evidence for this by providing a materialization based reasoner for acyclic ontologies which outperforms other state-of-the-art systems.
△ Less
Submitted 19 April, 2018;
originally announced April 2018.
-
On the Ontological Modeling of Trees
Authors:
David Carral,
Pascal Hitzler,
Hilmar Lapp,
Sebastian Rudolph
Abstract:
Trees -- i.e., the type of data structure known under this name -- are central to many aspects of knowledge organization. We investigate some central design choices concerning the ontological modeling of such trees. In particular, we consider the limits of what is expressible in the Web Ontology Language, and provide a reusable ontology design pattern for trees.
Trees -- i.e., the type of data structure known under this name -- are central to many aspects of knowledge organization. We investigate some central design choices concerning the ontological modeling of such trees. In particular, we consider the limits of what is expressible in the Web Ontology Language, and provide a reusable ontology design pattern for trees.
△ Less
Submitted 13 October, 2017;
originally announced October 2017.
