Reasoning about knowledge and time in asynchronous systems
Joseph Y. Halpern, Moshe Y. Vardi
STOC 1988
Datalog is the language of logic programs without function symbols. It is used as a database query language. If it is possible to eliminate recursion from a Datalog program II, then II is said to be bounded. It is known that the problem of deciding whether a given Datalog program is bounded is undecidable, even for binary programs. We show here that boundedness is decidable for monadic programs, i.e., programs where the recursive predicates are monadic (the non-recursive predicates can have arbitrary arity). Underlying our results are new tools for the optimization of Datalog programs based on automata theory and logic. In particular, one of the tools we develop is a theory of two-way alternating tree automata. We also use our techniques to show that containment for monadic programs is decidable. © 1988 ACM.
Joseph Y. Halpern, Moshe Y. Vardi
STOC 1988
Stavros S. Cosmadakis, Paris C. Kanellakis
SIGMOD/PODS 1986
Joseph Y. Halpern, Yoram Moses, et al.
STOC 1988
Haim Gaifman, Michael J. Maker, et al.
PODC 1991