Search

Let $C^2_p$ denote the class of first-order sentences with two variables and with additional quantifiers "there exists exactly (at most, at least) $i$" for $i\leq p$, and let $C^2$ be the union of $C^2_p$ taken over all integers $p$. We prove that the satisfiability problem for $C^2_1$ sentences is NEXPTIME-complete. This strengthens the results by [E. Gradel, Ph. Kolaitis, and M. Vardi, Bull. Symbolic Logic, 3 (1997), pp. 53--69], who showed that the satisfiability problem for the first-order two-variable logic $L^2$ is NEXPTIME-complete and by [E. Gradel, M. Otto, and E. Rosen, 12th Annual IEEE Symposium on Logic in Computer Science, 1997, pp. 306--317], who proved the decidability of $C^2$. Our result easily implies that the satisfiability problem for $C^2$ is in nondeterministic, doubly exponential time. It is interesting that $C^2_1$ is in NEXPTIME in spite of the fact that there are sentences whose minimal (and only) models are of doubly exponential size. It is worth noticing that by a recent result of [E. Gradel, M. Otto, and E. Rosen, Proceedings of 14th Annual Symposium on Theoretical Aspects of Computer Science, Lecture Notes in Comput. Sci. 1200, Springer-Verlag, Berlin, 1997], extensions of two-variable logic $L^2$ by a weak access to cardinalities through the Hartig (or equicardinality) quantifier is undecidable. The same is true for extensions of $L^2$ by very weak forms of recursion. The satisfiability problem for logics with a bounded number of variables has applications in artificial intelligence, notably in modal logics (see, e.g., [W. van der Hoek and M. De Rijke, J. Logic Comput., 5 (1995), pp. 325--345]), where counting comes in the context of graded modalities and in description logics, where counting can be used to express so-called number restrictions (see, e.g., [A. Borgida, Artificial Intelligence, 82 (1996), pp. 353--367]).

DATALOG is the language of logic programs without function symbols. It is considered to be the paradigmatic database query language. If it is possible to eliminate recursion from a DATALOG program then it is bounded. Since bounded programs can be executed in parallel constant time, the possibility of automatized boundedness detecting is believed to be an important issue and has been studied in many papers. Boundedness was proved to be undecidable for different kinds of semantical assumptions and syntactical restrictions. Many different proof techniques were used. In this paper we propose a uniform proof method based on the discovery of, as we call it, the Achilles--Turtle machine, and make strong improvements on most of the known undecidability results. In particular we solve the famous open problem of Kanellakis showing that uniform boundedness is undecidable for single rule programs (called also sirups). This paper is the full version of [J. Marcinkowski, Proc. 13th STACS, Lecture Notes in Computer Science 1046, pp. 427--438], and [J. Marcinkowski, 11th IEEE Symposium on Logic in Computer Science, pp. 13--24].