Datalog is a powerful rule-based language with numerous applications in databases and knowledge representation. Explaining why a fact belongs to the output of a Datalog program over a database is an essential task towards explainable and transparent data-intensive applications. A standard way of explaining a fact is the so-called why-provenance, which provides witnesses in the form of subsets of the input database that as a whole can be used to derive that fact. While why-provenance for Datalog has been extensively studied in the literature, the analogous notion for Datalog with negation remains unexplored. We extend why-provenance to Datalog with negation under the standard well-founded and stable model semantics, inherited from Logic Programming, by building on justification theory. We then perform a thorough data complexity analysis of the underlying explainability problem and show that it is in general intractable for both well-founded and stable model semantics; in particular, it is NP-complete, which is the best that we can hope for since the problem is already NP-complete for positive Datalog.

In recent years, explainable AI has become a major focus of research, driven by the need to better understand how AI systems arrive at their decisions in order to ensure trust and effective deployment. A central challenge in this field is the explanation of classifiers. Existing approaches typically distinguish between local explanations, which account for a classifier’s decision on an individual input, and global explanations, which aim to characterize the classifier’s behavior as a whole, independent of any particular input. This work concentrates on global explanations and characterizes classification decisions through "maximal" sufficient conditions that, when satisfied, guarantee that the classifier assigns the desired class to any input. We present a detailed analysis of the computational complexity of key problems in this setting across several important families of classifiers considered in the literature.

The chase procedure is a fundamental algorithmic tool in databases that allows us to reason with constraints, such as existential rules, with a plethora of applications. It takes a database and a set of constraints as input and iteratively completes the database as dictated by the constraints. A key challenge, though, is the fact that the chase may not terminate, which leads to the problem of checking whether it terminates given a database and a set of constraints. In this work, we focus on the semi-oblivious version of the chase, which is well-suited for practical implementations, and linear existential rules, a central class of constraints with several applications. In this setting, there is a mature body of theoretical work that provides syntactic characterizations of when the chase terminates, algorithms for checking chase termination, precise complexity results, and worst-case optimal bounds on the size of the result of the chase (whenever it is finite). Our main objective is to experimentally evaluate the existing chase termination algorithms with the aim of understanding which input parameters affect their performance, clarifying whether they can be used in practice, and revealing their performance limitations. Concerning guarded existential rules, a natural generalization of linear existential rules, one can reuse the machinery for linear existential rules by first applying the so-called linearization technique, that is, the technique of converting guarded existential rules into linear existential rules without affecting the termination of the chase. A secondary objective of this work is to understand how realistic is the use of the linearization technique in the context of the semi-oblivious chase termination problem.

Operational consistent query answering (CQA) is a recent framework for CQA, based on revised definitions of repairs and consistent answers, which opens up the possibility of efficient approximations with explicit error guarantees. The main idea is to iteratively apply operations (e.g., fact deletions), starting from an inconsistent database, until we reach a database that is consistent w.r.t. the given set of constraints. This gives us the flexibility of choosing the probability with which we apply an operation, which in turn allows us to calculate the probability of an operational repair, and thus, the probability with which a consistent answer is entailed. A natural way of assigning probabilities to operations is by targeting the uniform probability distribution over a reasonable space such as the set of operational repairs, the set of sequences of operations that lead to an operational repair, and the set of available operations at a certain step of the repairing process. This leads to what we generally call uniform operational CQA. The goal of this work is to perform a data complexity analysis of both exact and approximate uniform operational CQA, focusing on functional dependencies (and subclasses thereof) and conjunctive queries. The main outcome of our analysis, among other positive and negative results, is that uniform operational CQA pushes the efficiency boundaries further by ensuring the existence of efficient approximation schemes in scenarios that go beyond the simple case of primary keys, which seems to be the limit of the classical approach to CQA.

Existential rules, a.k.a. tuple-generating dependencies (TGDs), form a well-established formalism for specifying ontologies. In particular, the warded language is a well-behaved fragment of TGD-based ontologies, striking a good balance between expressive power and computational complexity of answering Ontology-Mediated Queries (OMQs). The theoretical foundations of answering OMQs over warded ontologies are by now well-understood, but to the best of our knowledge, very few efforts exist that exploit such a rich theory for building practical query answering algorithms. Our goal is to fill the above gap by designing a novel Datalog rewriting algorithm for OMQs over warded ontologies which is amenable to practical implementations, as well as providing an implementation and an experimental evaluation, with the aim of understanding how key input parameters affect the performance of this approach, and what are its limits when combined with off-the-shelf Datalog-based engines.

Rule-based languages lie at the core of several areas of central importance to databases and artificial intelligence such as deductive databases and knowledge representation and reasoning. Disjunctive existential rules (a.k.a. disjunctive tuple-generating dependencies in the database literature) form such a prominent rule-based language. The goal of this work is to pinpoint the expressive power of disjunctive existential rules in terms of insightful model-theoretic properties. More precisely, given a collection C of relational structures, we show that C is axiomatizable via a finite set R of disjunctive existential rules (i.e., C is precisely the set of models of R) iff C enjoys certain model-theoretic properties. This is achieved by using the well-known property of criticality, a refined version of closure under direct products, and a novel property called diagrammatic compatibility that relies on the method of diagrams. We further establish analogous characterizations for the well-behaved classes of linear and guarded disjunctive existential rules by adopting refined versions of diagrammatic compatibility that consider the syntactic restrictions imposed by linearity and guardedness; this illustrates the robustness of diagrammatic compatibility. We finally exploit diagrammatic compatibility to rewrite a set of guarded disjunctive existential rules into an equivalent set that falls in the weaker class of linear disjunctive existential rules, if one exists.

Explainable AI has garnered considerable attention in recent years, as understanding the reasons behind decisions made by AI systems is crucial for their successful adoption. Explaining classifiers' behavior is one prominent problem. Work in this area has proposed notions of both local and global explanations, where the former are concerned with explaining a classifier's behavior for a specific instance, while the latter are concerned with explaining the overall classifier's behavior regardless of any specific instance. In this paper, we focus on global explanations, and explain classification in terms of ``minimal'' necessary conditions for the classifier to assign a specific class to a generic instance. We carry out a thorough complexity analysis of the problem for natural minimality criteria and important families of classifiers considered in the literature.

Explaining an answer to a Datalog query is an essential task towards Explainable AI, especially nowadays where Datalog plays a critical role in the development of ontology-based applications. A well-established approach for explaining a query answer is the so-called why-provenance, which essentially collects all the subsets of the input database that can be used to obtain that answer via some derivation process, typically represented as a proof tree. It is well known, however, that computing the why-provenance for Datalog queries is computationally expensive, and thus, very few attempts can be found in the literature. The goal of this work is to demonstrate how off-the-shelf SAT solvers can be exploited towards an efficient computation of the why-provenance for Datalog queries. Interestingly, our SAT-based approach allows us to build the why-provenance in an incremental fashion, that is, one explanation at a time, which is much more useful in a practical context than the one-shot computation of the whole set of explanations as done by existing approaches.

Datalog is a powerful rule-based language that allows us to express complex recursive queries and has found numerous applications over the years. Explaining why a result to a Datalog query is obtained is an essential task towards explainable and transparent data-intensive applications that rely on Datalog. A standard way of explaining a query result is the so-called why-provenance, which provides information about the witnesses to a query result in the form of subsets of the input database that as a whole can be used to derive that result. To our surprise, despite the fact that the notion of why-provenance for Datalog queries has been around for decades and intensively studied, its computational complexity remains unexplored. Our goal is to fill this gap in the why-provenance literature. Towards this end, we pinpoint the data complexity of why-provenance for Datalog queries and key subclasses thereof. The takeaway of our work is that why-provenance for recursive queries, even if the recursion is limited to be linear, is an intractable problem, whereas for non-recursive queries is highly tractable.

Operational consistent query answering (CQA) is a recent framework for CQA based on revised definitions of repairs, which are built by applying a sequence of operations (e.g., fact deletions) starting from an inconsistent database until we reach a database that is consistent w.r.t. the given set of constraints. It has been recently shown that there is an efficient approximation for computing the percentage of repairs that entail a given query when we focus on primary keys, conjunctive queries, and assuming the query is fixed (i.e., in data complexity). However, it has been left open whether such an approximation exists when the query is part of the input (i.e., in combined complexity). We show that this is the case when we focus on self-join-free conjunctive queries of bounded generelized hypertreewidth. We also show that it is unlikely that efficient approximation schemes exist once we give up one of the adopted syntactic restrictions, i.e., self-join-freeness or bounding the generelized hypertreewidth. Towards the desired approximation, we introduce a counting complexity class, called SpanTL, show that each problem in it admits an efficient approximation scheme by using a recent approximability result about tree automata, and then place the problem of interest in SpanTL.

Datalog is a well-established rule-based language that allows us to express complex recursive queries. As for every other query language, explaining why a result to a Datalog query is obtained is an essential task towards explainable and transparent query evaluation. A standard way of explaining a query result is the so-called why-provenance, which provides information about the witnesses to a query result in the form of subsets of the input database that as a whole can be used to derive that result. The data complexity of why-provenance for Datalog queries has been recently studied and it was shown to be intractable, namely NP-complete even if the recursion is linear. An interesting question that comes up is whether we can ensure tractable data complexity by considering a slightly less informative notion of provenance, in particular, whyminimal-provenance that keeps only subset-minimal witnesses to a query result. Another interesting question is whether we can adopt a more informative notion of provenance than why-provenance, in particular, whymultiplicity-provenance that also keeps track of how many times a certain fact occurs in a witness to a query result, without paying a price in data complexity. This work provides definitive answers to the above questions: (i) whyminimal-provenance ensures tractable data complexity, and (ii) whymultiplicity-provenance can be adopted without paying a price in complexity, apart from one surprising case where the data complexity becomes PSPACE-complete.

Abstract Data exchange, the problem of transferring data from a source schema to a target schema, has been studied for several years. The semantics of answering positive queries over the target schema has been defined in early work, but little attention has been paid to more general queries. A few proposals of semantics for more general queries exist but they either do not properly extend the standard semantics under positive queries, giving rise to counterintuitive answers, or they make query answering undecidable even for the most important data exchange settings, for example, with weakly-acyclic dependencies. The goal of this paper is to provide a new semantics for data exchange that is able to deal with general queries. At the same time, we want our semantics to coincide with the classical one when focusing on positive queries, and to not trade-off too much in terms of complexity of query answering. We show that query answering is undecidable in general under the new semantics, but it is $\text{co}\text{NP}\text{-complete}$ when the dependencies are weakly-acyclic. Moreover, in the latter case, we show that exact answers under our semantics can be computed by means of logic programs with choice, thus exploiting existing efficient systems. For more efficient computations, we also show that our semantics allows for the construction of a representative target instance, similar in spirit to a universal solution, that can be exploited for computing approximate answers in polynomial time.

Dung's Argumentation Framework (AF) has been extended in several directions, including the possibility of representing uncertainty about the existence of arguments and attacks. In this regard, two main proposals have been introduced in the literature: Probabilistic Argumentation Framework (PrAF) and Incomplete Argumentation Framework (iAF). PrAF is an extension of AF with probability theory, thus representing quantified uncertainty. In contrast, iAF represents unquantified uncertainty, that is it can be seen as a special case where we only know that some elements (arguments or attacks) are uncertain. In this paper, we first address the problem of computing the probability that a given argument is accepted in PrAF. This is carried out by introducing the concept of probabilistic explanation for any given (probabilistic) extension. We show that the complexity of the problem is FP#P-hard and propose polynomial approximation algorithms with bounded additive error for PrAFs where odd-length cycles are forbidden. We investigate the approximate complexity of the related FP#P-hard problems of credulous and skeptical acceptance in PrAF, showing that they are generally harder than the problem of computing the probability that a given argument is accepted. Next we consider iAF and, after showing some equivalence properties among classes of iAFs, we study iAF as a special case of PrAF where uncertain elements have associated a probability equal to 1/2. Finally, given this result, we investigate the relationships between iAF acceptance problems and probabilistic acceptance in PrAF.

The chase procedure is a fundamental algorithmic tool in databases that allows us to reason with constraints, such as existential rules, with a plethora of applications. It takes as input a database and a set of constraints, and iteratively completes the database as dictated by the constraints. A key challenge, though, is the fact that it may not terminate, which leads to the problem of checking whether it terminates given a database and a set of constraints. In this work, we focus on the semi-oblivious version of the chase, which is well-suited for practical implementations, and linear existential rules, a central class of constraints with several applications. In this setting, there is a mature body of theoretical work that provides syntactic characterizations of when the chase terminates, algorithms for checking chase termination, and precise complexity results. Our main objective is to experimentally evaluate the existing chase termination algorithms with the aim of understanding which input parameters affect their performance, clarifying whether they can be used in practice, and revealing their performance limitations.

The chase procedure, originally introduced for checking implication of database constraints, and later on used for computing data exchange solutions, has recently become a central algorithmic tool in rule-based ontological reasoning. In this context, a key problem is non-uniform chase termination: does the chase of a database w.r.t. a rule-based ontology terminate? And if this is the case, what is the size of the result of the chase? We focus on guarded tuple-generating dependencies (TGDs), which form a robust rule-based ontology language, and study the above central questions for the semi-oblivious version of the chase. One of our main findings is that non-uniform semi-oblivious chase termination for guarded TGDs is feasible in polynomial time w.r.t. the database, and the size of the result of the chase (whenever is finite) is linear w.r.t. the database. Towards our results concerning non-uniform chase termination, we show that basic techniques such as simplification and linearization, originally introduced in the context of ontological query answering, can be safely applied to the chase termination problem.

Operational consistent query answering (CQA) is a recent framework for CQA, based on revised definitions of repairs and consistent answers, which opens up the possibility of efficient approximations with explicit error guarantees. The main idea is to iteratively apply operations (e.g., fact deletions), starting from an inconsistent database, until we reach a database that is consistent w.r.t. the given set of constraints. This gives us the flexibility of choosing the probability with which we apply an operation, which in turn allows us to calculate the probability of an operational repair, and thus, the probability with which a consistent answer is entailed. A natural way of assigning probabilities to operations is by targeting the uniform probability distribution over a reasonable space such as the set of operational repairs, the set of sequences of operations that lead to an operational repair, and the set of available operations at a certain step of the repairing process. This leads to what we generally call uniform operational CQA. The goal of this work is to perform a data complexity analysis of both exact and approximate uniform operational CQA, focusing on functional dependencies (and subclasses thereof), and conjunctive queries. The main outcome of our analysis (among other positive and negative results), is that uniform operational CQA pushes the efficiency boundaries further by ensuring the existence of efficient approximation schemes in scenarios that go beyond the simple case of primary keys, which seems to be the limit of the classical approach to CQA.

A key task in the context of consistent query answering is to count the number of repairs that entail the query, with the ultimate goal being a precise data complexity classification. This has been achieved in the case of primary keys and self-join-free conjunctive queries (CQs) via an FP/#P-complete dichotomy. We lift this result to the more general case of functional dependencies (FDs). Another important task in this context is whenever the counting problem in question is intractable, to classify it as approximable, i.e., the target value can be efficiently approximated with error guarantees via a fully polynomial-time randomized approximation scheme (FPRAS), or as inapproximable. Although for primary keys and CQs (even with self-joins) the problem is always approximable, we prove that this is not the case for FDs. We show, however, that the class of FDs with a left-hand side chain forms an island of approximability. We see these results, apart from being interesting in their own right, as crucial steps towards a complete classification of approximate counting of repairs in the case of FDs and self-join-free CQs.

Consistent query answering (CQA) aims to deliver meaningful answers when queries are evaluated over inconsistent databases. Such answers must be certainly true in all repairs, which are consistent databases whose difference from the inconsistent one is somehow minimal. Although CQA provides a clean framework for querying inconsistent databases, it is arguably more informative to compute the percentage of repairs in which a candidate answer is true, instead of simply saying that is true in all repairs, or is false in at least one repair. It should not be surprising, though, that computing this percentage is computationally hard. On the other hand, for practically relevant settings such as conjunctive queries and primary keys, there are data-efficient randomized approximation schemes for approximating this percentage. Our goal is to perform a thorough experimental evaluation and comparison of those approximation schemes. Our analysis provides new insights on which technique is indicated depending on key characteristics of the input, and it further provides evidence that making approximate CQA as described above feasible in practice is not an unrealistic goal.

Abstract The chase procedure is a fundamental algorithmic tool in database theory with a variety of applications. A key problem concerning the chase procedure is all-instances termination: for a given set of tuple-generating dependencies (TGDs), is it the case that the chase terminates for every input database? In view of the fact that this problem is undecidable, it is natural to ask whether known well-behaved classes of TGDs, introduced in different contexts such as ontological reasoning, ensure decidability. We consider a prominent paradigm that led to a robust TGD-based formalism, called stickiness. We show that for sticky sets of TGDs, all-instances chase termination is decidable if we focus on the (semi-)oblivious chase, and we pinpoint its exact complexity: PSpace -complete in general, and NLogSpace -complete for predicates of bounded arity. These complexity results are obtained via a graph-based syntactic characterization of chase termination that is of independent interest.

Consistent query answering is a principled approach for querying inconsistent databases. It relies on two basic notions: the notion of a repair, that is, a consistent database that "minimally" differs from the original one, and the notion of a consistent query answer, that is, a query answer that can be derived from every repair. In general, an inconsistent database can admit multiple repairs, each corresponding to a different way of restoring consistency, and the consistent query answering framework does not make any discrimination among them. However, in many applications it is natural and desired to express preferences among the different choices that can be made to resolve inconsistency.

Recently there has been an increasing interest in probabilistic abstract argumentation, an extension of Dung's abstract argumentation framework with probability theory. In this setting, we address the problem of computing the probability that a given argument is accepted. This is carried out by introducing the concept of probabilistic explanation for a given (probabilistic) extension. We show that the complexity of the problem is FP^#P-hard and propose polynomial approximation algorithms with bounded additive error for probabilistic argumentation frameworks where odd-length cycles are forbidden. This is quite surprising since, as we show, such kind of approximation algorithm does not exist for the related FP^#P-hard problem of computing the probability of the credulous acceptance of an argument, even for the special class of argumentation frameworks considered in the paper.

Query answering over inconsistent knowledge bases is a problem that has attracted a great deal of interest over the years. Different inconsistency-tolerant semantics have been proposed, and most of them are based on the notion of repair, that is, a "maximal" consistent subset of the database. In general, there can be several repairs, so it is often natural and desirable to express preferences among them. In this paper, we propose a framework for querying inconsistent knowledge bases under user preferences for existential rule languages. We provide generalizations of popular inconsistency-tolerant semantics taking preferences into account and study the data and combined complexity of different relevant problems.

The chase procedure is one of the most fundamental algorithmic tools in database theory. A key algorithmic task is uniform chase termination, i.e., given a set of tuple-generating dependencies (tgds), is it the case that the chase under this set of tgds terminates, for every input database? In view of the fact that this problem is undecidable, no matter which version of the chase we consider, it is natural to ask whether well-behaved classes of tgds, introduced in different contexts such as ontological reasoning, make our problem decidable. In this work, we consider a prominent decidability paradigm for tgds, called stickiness. We show that for sticky sets of tgds, uniform chase termination is decidable if we focus on the (semi-)oblivious chase, and we pinpoint its exact complexity: PSpace-complete in general, and NLogSpace-complete for predicates of bounded arity. These complexity results are obtained via graph-based syntactic characterizations of chase termination that are of independent interest.

Consistent query answering (CQA) aims to deliver meaningful answers when queries are evaluated over inconsistent databases. Such answers must be certainly true in all repairs, which are consistent databases whose difference from the inconsistent one is somehow minimal. An interesting task in this context is to count the number of repairs that entail the query. This problem has been already studied for conjunctive queries and primary keys; we know that it is #P-complete in data complexity under polynomial-time Turing reductions (a.k.a. Cook reductions). However, as it has been already observed in the literature of counting complexity, there are problems that are ''hard-to-count-easy-to-decide'', which cannot be complete (under reasonable assumptions) for #P under weaker reductions, and, in particular, under standard many-one logspace reductions (a.k.a. parsimonious reductions). For such ''hard-to-count-easy-to-decide'' problems, a crucial question is whether we can determine their exact complexity by looking for subclasses of #P to which they belong. Ideally, we would like to show that such a problem is complete for a subclass of #P under many-one logspace reductions. The main goal of this work is to perform such a refined analysis for the problem of counting the number of repairs under primary keys that entail the query.

Consistent query answering (CQA) aims to find meaningful answers to queries when databases are inconsistent, i.e., do not conform to their specifications. Such answers must be certainly true in all repairs, which are consistent databases whose difference from the inconsistent one is minimal, according to some measure. This task is often computationally intractable, and much of CQA research concentrated on finding islands of tractability. Nevertheless, there are many relevant queries for which no efficient solutions exist, which is reflected by the limited practical applicability of the CQA approach. To remedy this, one needs to devise a new CQA framework that provides explicit guarantees on the quality of query answers. However, the standard notions of repair and certain answers are too coarse to permit more elaborate schemes of query answering. Our goal is to provide a new framework for CQA based on revised definitions of repairs and query answering that opens up the possibility of efficient approximate query answering with explicit guarantees. The key idea is to replace the current declarative definition of a repair with an operational one, which explains how a repair is constructed, and how likely it is that a consistent instance is a repair. This allows us to define how certain we are that a tuple should be in the answer. Using this approach, we study the complexity of both exact and approximate CQA. Even though some of the problems remain hard, for many common classes of constraints we can provide meaningful answers in reasonable time, for queries going far beyond the standard CQA approach.

In this article, we propose a new technique for checking whether the bottom-up evaluation of logic programs with function symbols terminates. The technique is based on the definition of mappings from arguments to strings of function symbols, representing possible values which could be taken by arguments during the bottom-up evaluation. Starting from mappings, we identify mapping-restricted arguments, a subset of limited arguments, namely arguments that take values from finite domains. Mapping-restricted programs, consisting of rules whose arguments are all mapping restricted, are terminating under the bottom-up computation, as all of its arguments take values from finite domains. We show that mappings can be computed by transforming the original program into a unary logic program: this allows us to establish decidability of checking if a program is mapping restricted. We study the complexity of the presented approach and compare it to other techniques known in the literature. We also introduce an extension of the proposed approach that is able to recognize a wider class of logic programs. The presented technique provides a significant improvement, as it can detect terminating programs not identified by other criteria proposed so far. Furthermore, it can be combined with other techniques to further enlarge the class of programs recognized as terminating under the bottom-up evaluation.

The chase is a well-known algorithm with a wide range of applications in data exchange, data cleaning, data integration, query optimization, and ontological reasoning. Since the chase evaluation might not terminate and it is undecidable whether it terminates, the problem of defining (decidable) sufficient conditions ensuring termination has received a great deal of interest in recent years. In this regard, several termination criteria have been proposed. One of the main weaknesses of current approaches is the limited analysis they perform on equality generating dependencies (EGDs). In this paper, we propose sufficient conditions ensuring that a set of dependencies has at least one terminating chase sequence. We propose novel criteria which are able to perform a more accurate analysis of EGDs. Specifically, we propose a new stratification criterion and an adornment algorithm. The latter can both be used as a termination criterion and be combined with current techniques to make them more effective, in that strictly more sets of dependencies are identified. Our techniques identify sets of dependencies that are not recognized by any of the current criteria.

Abstract It is widely acknowledged that function symbols are an important feature in answer set programming, as they make modelling easier, increase the expressive power, and allow us to deal with infinite domains. The main issue with their introduction is that the evaluation of a program might not terminate and checking whether it terminates or not is undecidable. To cope with this problem, several classes of logic programs have been proposed where the use of function symbols is restricted but the program evaluation termination is guaranteed. Despite the significant body of work in this area, current approaches do not include many simple practical programs whose evaluation terminates. In this paper, we present the novel classes ofrule-boundedandcycle-bounded programs, which overcome different limitations of current approaches by performing a more global analysis of how terms are propagated from the body to the head of rules. Results on the correctness, the complexity, and the expressivity of the proposed approach are provided.

The chase procedure is considered as one of the most fundamental algorithmic tools in database theory. It has been successfully applied to different database problems such as data exchange, and query answering and containment under constraints, to name a few. One of the central problems regarding the chase procedure is all-instance termination, that is, given a set of tuple-generating dependencies (TGDs) (a.k.a. existential rules), decide whether the chase under that set terminates, for every input database. It is well-known that this problem is undecidable, no matter which version of the chase we consider. The crucial question that comes up is whether existing restricted classes of TGDs, proposed in different contexts such as ontological query answering, make the above problem decidable. In this work, we focus our attention on the oblivious and the semi-oblivious versions of the chase procedure, and we give a positive answer for classes of TGDs that are based on the notion of guardedness. To the best of our knowledge, this is the first work that establishes positive results about the (semi-)oblivious chase termination problem. In particular, we first concentrate on the class of linear TGDs, and we syntactically characterize, via rich- and weak-acyclicity, its fragments that guarantee the termination of the oblivious and the semi-oblivious chase, respectively. Those syntactic characterizations, apart from being interesting in their own right, allow us to pinpoint the complexity of the problem, which is PSPACE-complete in general, and NL-complete if we focus on predicates of bounded arity, for both the oblivious and the semi-oblivious chase. We then proceed with the more general classes of guarded and weakly-guarded TGDs. Although we do not provide syntactic characterizations for its relevant fragments, as for linear TGDs, we show that the problem under consideration remains decidable. In fact, we show that it is 2EXPTIME-complete in general, and EXPTIME-complete if we focus on predicates of bounded arity, for both the oblivious and the semi-oblivious chase. Finally, we investigate the expressive power of the query languages obtained from our analysis, and we show that they are equally expressive with standard database query languages. Nevertheless, we have strong indications that they are more succinct.

Abstract Recently, there has been an increasing interest in the bottom-up evaluation of the semantics of logic programs with complex terms. The presence of function symbols in the program may render the ground instantiation infinite, and finiteness of models and termination of the evaluation procedure, in the general case, are not guaranteed anymore. Since the program termination problem is undecidable in the general case, several decidable criteria (called program termination criteria) have been recently proposed. However, current conditions are not able to identify even simple programs, whose bottom-up execution always terminates. The paper introduces new decidable criteria for checking termination of logic programs with function symbols under bottom-up evaluation, by deeply analyzing the program structure. First, we analyze the propagation of complex terms among arguments by means of the extended version of the argument graph calledpropagation graph. The resulting criterion, calledacyclicity, generalizes most of the decidable criteria proposed so far. Next, we study how rules may activate each other and define a more powerful criterion, calledsafety. This criterion uses the so-calledsafety functionable to analyze how rules may activate each other and how the presence of some arguments in a rule limits its activation. We also study the application of the proposed criteria to bound queries and show that the safety criterion is well-suited to identify relevant classes of programs and bound queries. Finally, we propose a hierarchy of classes of terminating programs, calledk-safety, where thek-safe class strictly includes the (k-1)-safe class.

In this paper we propose a new technique for checking whether the bottom-up evaluation of logic programs with function symbols terminates. The technique is based on the definition of mappings from arguments to strings of function symbols, representing possible values which could be taken by arguments during the bottom-up evaluation. Such mappings can be computed by transforming the original program into a unary logic program whose termination is decidable. Starting from mappings we can identify mapping-restricted arguments, a subset of limited arguments, that is, arguments which can take values from finite domains. The class of mapping-restricted programs, consisting of programs whose arguments are mapping-restricted, is terminating under the bottom-up computation as all its arguments can take values from finite domains. We study the complexity of the presented approach and compare it with other techniques known in the literature. The presented technique is relevant as it individuates as terminating programs not detected by other criteria proposed so far and can be combined with other techniques to further enlarge the class of programs recognized as terminating under the bottom-up evaluation.