Fixpoint semantics and optimization of recursive Datalog programs with aggregates

A very desirable Datalog extension investigated by many researchers in the last 30 years consists in allowing the use of the basic SQL aggregates min, max, count and sum in recursive rules. In this paper, we propose a simple comprehensive solution that extends the declarative least-fixpoint semantics of Horn Clauses, along with the optimization techniques used in the bottom-up implementation approach adopted by many Datalog systems. We start by identifying a large class of programs of great practical interest in which the use of min or max in recursive rules does not compromise the declarative fixpoint semantics of the programs using those rules. Then, we revisit the monotonic versions of count and sum aggregates proposed by Mazuran et al. (2013b, The VLDB Journal 22, 4, 471–493) and named, respectively, mcount and msum. Since mcount, and also msum on positive numbers, are monotonic in the lattice of set-containment, they preserve the fixpoint semantics of Horn Clauses. However, in many applications of practical interest, their use can lead to inefficiencies, that can be eliminated by combining them with max, whereby mcount and msum become the standard count and sum. Therefore, the semantics and optimization techniques of Datalog are extended to recursive programs with min, max, count and sum, making possible the advanced applications of superior performance and scalability demonstrated by BigDatalog (Shkapsky et al. 2016. In SIGMOD. ACM, 1135–1149) and Datalog-MC (Yang et al. 2017. The VLDB Journal 26, 2, 229–248).

A declarative extension of horn clauses, and its significance for datalog and its applications

FS-rules provide a powerful monotonic extension for Horn clauses that supports monotonic aggregates in recursion by reasoning on the multiplicity of occurrences satisfying existential goals. The least fixpoint semantics, and its equivalent least model semantics, hold for logic programs with FS-rules; moreover, generalized notions of stratification and stable models are easily derived when negated goals are allowed. Finally, the generalization of techniques such as seminaive fixpoint and magic sets, make possible the efficient implementation of DatalogFS, i.e., Datalog with rules with Frequency Support (FS-rules) and stratified negation. A large number of applications that could not be supported efficiently, or could not be expressed at all in stratified Datalog can now be easily expressed and efficiently supported in DatalogFS and a powerful DatalogFS system is now being developed at UCLA.

A FRAMEWORK FOR HANDLING LOGICAL INCONSISTENCIES IN THE FUSION OF BOOLEAN KNOWLEDGE BASES

In this paper, a framework for fusing several Boolean knowledge bases together is presented. The focus is on detecting inconsistencies and overcoming them so that a consistent global knowledge base is obtained. The framework is based on two cornerstones: detecting inconsistencies using algorithmic techniques to compute minimally unsatisfiable sub-formulas, and adopting a logic-based weakening approach to restore consistency for the fused knowledge. The dynamics in the framework in terms of both model-theoretic and the fixpoint semantics is then investigated.

(Co-)Inductive semantics for Constraint Handling Rules

In this paper, we address the problem of defining a fixpoint semantics for Constraint Handling Rules (CHR) that captures the behavior of both simplification and propagation rules in a sound and complete way with respect to their declarative semantics. Firstly, we show that the logical reading of states with respect to a set of simplification rules can be characterized by a least fixpoint over the transition system generated by the abstract operational semantics of CHR. Similarly, we demonstrate that the logical reading of states with respect to a set of propagation rules can be characterized by the greatest fixpoint. Then, in order to take advantage of both types of rules without losing fixpoint characterization, we present a new operational semantics with persistent constraints.We finally establish that this semantics can be characterized by two nested fixpoints, and we show that the resulting language is an elegant framework to program using coinductive reasoning.

A Fixpoint Semantics for Rule-Base Anomalies

A crucial component of an intelligent system is its knowledge base that contains knowledge about a problem domain. Knowledge base development involves domain analysis, context space definition, ontological specification, and knowledge acquisition, codification and verification. Knowledge base anomalies can affect the correctness and performance of an intelligent system. In this chapter, we describe a fixpoint semantics for a knowledge base that is based on a multi-valued logic. We then use the fixpoint semantics to provide formal definitions for four types of knowledge base anomalies: inconsistency, redundancy, incompleteness, circularity. We believe such formal definitions of knowledge base anomalies will help pave the way for a more effective knowledge base verification process.