Reference: Levy, A. Y.; Mumick, I. S.; Sagiv, Y.; & Shmueli, O. Equivalence, Query-reachability and Satisfiability in Datalog Extensions. 1993.
Abstract: We consider the problems of query-reachability and satisfiability in datalog programs with negation and dense- order constraints. These problems are important in the context of optimization, since solving them can detect extraneous rules and predicates. Satisfiability was shown decidable for pure datalog programs~\cite{Shmu87}; decidability for datalog with dense-order constraints follows from the work of~\cite{KKR90}. Query-reachability was shown decidable for datalog with dense-order constraints~\cite{LS92}. In this paper, we show that both query-reachability and satisfiability are decidable for datalog programs with dense-order constraints and safe stratified negation provided that negation is applied only to EDB predicates, or all EDB predicates are unary. We also give a new undecidability result for satisfiability that implies a new undecidability result for both query- reachability and equivalence. These undecidability results apply to datalog programs with unary IDB predicates, negation, and the interpreted predicate $\not=$. In comparison, note that equivalence is decidable for datalog programs with only unary IDB predicates (and neither negation nor interpreted predicates)~\cite{CGKV88}. In proving some of the decidability results, we use a rather powerful tool, the {\em query-tree,} which was first used in~\cite{LS92}. A query-tree is a finite structure that encodes all symbolic derivation trees (of a datalog program $P$) that satisfy some given property. Query-trees can also be viewed as a refinement of tree automata techniques for the special purpose of representing symbolic derivation trees of datalog programs. The importance of tree-automata techniques for decision problems of datalog programs was shown in~\cite{Vard89}. Query-trees can be used not just for decision problems, but also for analyzing datalog programs and transforming those programs into more efficient ones. For example, using query-trees, it is rather easy to push the tightest possible constraints to the EDB, and to use constraints most efficiently during a magic-set evaluation. Conceivably the same could be done by applying tree-automata techniques directly, but doing so would be considerably more intricate. So, in essence, our results do not merely provide new decidable cases, but also imply how to push constraints in those cases.
Notes: April.
Full paper available as ps.