Set constraints form a constraint system where variables range over the domain of sets of trees. They give a natural formalism for many problems in program analysis. Syntactically, set constraints are conjunctions of inclusions between expressions built over variables, constructors (constants and function symbols from a given signature) and a choice of set operators that defines the specific class of set constraints. In this article, we are interested in the class of set constraints with projections , which is the class with all Boolean operators (union, intersection and complement) and projections that in program analysis directly correspond to type destructors. We prove that the problem of existence of a solution of a system of set constraints with projections is in NEXPTIME, and thus that it is NEXPTIME-complete.

The possibility of creating machine intelligence superior to human intelligence seems to derive from the outcome of Moore's principle, describing exponential increases of calculative speed and capacity of computers. On the basis of the so-far performed analyses, it can be presumed that around the year 2020, the calculative capacity of personal computers will match the capacity of the human brain. If there is no breakdown of this trend, then ten years after, the capacity will reach a level comparable with the size of all brains of all the people in the world. According to the idea of the grid computing, the possibility of downloading to such a “machine” that has all our mental make-up (recorded in neuron structures) will become achievable. The possibility of a human mastering the snowballing development of artificial intelligence lays in constructing a neural interface. The second way of integrating human mind with cyberspace is connected with building computers operating on the basis of a neural network principle. The previously mentioned two ways should be perceived as priority of ergonomic issues of the neural integrated human–computer interaction.

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. Grädel, 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. Grädel, 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. Grädel, 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 Härtig (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]).

Let C/sub k//sup 2/ denote the class of first order sentences with two variables and with additional quantifiers "there exists exactly (at most, at least) m", for m/spl les/k, and let C/sup 2/ be the union of C/sub k//sup 2/ taken over all integers k. We prove that the problem of satisfiability of sentences of C/sub 1//sup 2/ is NEXPTIME-complete. This strengthens a recent result of E. Gradel, Ph. Kolaitis and M. Vardi (1997) who proved that the satisfiability problem for the first order two-variable logic L/sup 2/ is NEXPTIME-complete and a very recent result by E. Gradel, M. Otto and E. Rosen (1997) who proved the decidability of C/sup 2/. Our result easily implies that the satisfiability problem for C/sup 2/ is in non-deterministic, doubly exponential time. It is interesting that C/sub 1//sup 2/ is in NEXPTIME in spite of the fact, that there are sentences whose minimal (and only) models are of doubly exponential size.

The exponent of periodicity is an important factor in estimates of complexity of word-unification algorithms. We prove that the exponent of periodicity of a minimal solution of a word equation is of order 2 1.07d , where d is the length of the equation. We also give a lower bound 2 0.29d so our upper bound is almost optimal and exponentially better than the original bound (6d) 22d4 + 2 . Consequently, our result implies an exponential improvement of known upper bounds on complexity of word-unification algorithms.

Systems of set constraints describe relations between sets of ground terms. They have been successfully used in program analysis and type inference. In this paper we prove that the problem of existence of a solution of a system of set constraints with projections is in NEXPTIME, and thus that it is NEXPTIME-complete. This extends the result of A. Aiken, D. Kozen, and E.L. Wimmers (1993) and R. Gilleron, S. Tison, and M. Tommasi (1990) on decidability of negated set constraints and solves a problem that was open for several years.>

Systems of set constraints describe relations between sets of ground terms. They have been successfully used in program analysis and type inference. So far two proofs of decidability of mixed set constraints have been given: by R. Gilleron, S. Tison and M. Tommasi (1993) and A. Aiken, D. Kozen, and E.L. Wimmers (1993). However, both these proofs are long, involved and do not seem to extend to more general set constraints. Our approach is based on a reduction of set constraints to the monadic class given in a paper by L. Bachmair, H. Ganzinger, and U. Waldmann (1993). We first give a new proof of decidability of systems of mixed (positive and negative) set constraints. We explicitly describe a very simple algorithm working in NEXPTIME and we give in all detail a relatively easy proof of its correctness. Then, we sketch how our technique can be applied to get various extensions of this result. In particular we prove that the problem of consistency of mixed set constraints with restricted projections and unrestricted diagonalization is in NEXPTIME.>

The authors prove that the problem 'given two Horn clauses H/sub 1/=( alpha /sub 1/ V-product alpha /sub 2/ to beta ) and H/sub 2/=( gamma /sub 1/ V-product . . . V-product gamma /sub k/ to delta ), where alpha /sub i/, beta , gamma /sub i/, delta are atomic formulas, decide if H/sub 2/, is a consequence of H/sub 1/' is not recursive. This solves one of the last open decidability problems concerning formulas in pure predicate logic (i.e. without equality symbol). The proof depends on a thorough analysis of derivation trees of one rule of inference with two premisses and one conclusion, and it may have further applications.>

It is proved that the 0-1 law does not hold for the class of existential second sentences whose first order part is in the minimal Godel class, i.e. has the quantifier prenex consisting of two universal quantifiers followed by just one existential quantifier. This completes the classification of existential second order sentences for which the 0-1 law holds. It is also proved that asymptotic probabilities of sentences as above form a dense subset of the unit interval.>

In [9] and [10] P. Kolaitis and M. Vardi proved that the 0-1 law holds for the second-order existential sentences whose first-order parts are formulas of Bernays-Schonfinkel or Ackermann prefix classes. They also provided several examples of second-order formulas for which the 0-1 law does not hold, and noticed that the classification of second-order sentences for which the 0-1 law holds resembles the classification of decidable cases of first-order prenex sentences. The only cases they have not settled are the cases of Gödel classes with and without equality. In this paper we confirm the conjecture of Kolaitis and Vardi that the 0-1 law does not hold for the existential second-order sentences whose first-order part is in Gödel prenex form with equality. The proof we give is based on a modification of the example employed by W. Goldfarb [5] in his proof that, contrary to the Gödel claim [6], the class of Gödel prenex formulas with equality is undecidable.

It is proved that the exponent of periodicity of a minimal solution of a word equation is at most 2/sup 2.54n/, where n is the length of the equation. Since the best known lower bound is 2/sup 0.31n/, this upper bound is almost optimal and exponentially better than the original bound. Thus the result implies exponential improvement of known upper bounds on complexity of word-unification algorithms. Evidence is given that, contrary to common belief, the algorithm deciding satisfiability of equations in free groups, given by G.S. Makanin (1977), is not primitive recursive.>

P. Kolaitis and M. Vardi (see Proc. 19th ACM Symp. on Theory of Computing, p.425-35 (1987), and Proc. 3rd Ann. Symp. on Logic in Computer Science, p.2-11 (1988)) proved that the 0-1 law holds for the second-order existential sentences whose first-order parts are formulas of Bernays-Schonfinkel or Ackermann prefix classes. They also provided several examples of second-order formulas for which the 0-1 law does not hold and noticed that the classification of second-order sentences for which the 0-1 law holds resembles the classification of decidable cases of prenex first-order sentences. The only cases they have not settled were the cases of Godel classes with and without equality. The authors confirm the conjecture of Kolaitis and Vardi that the 0-1 law does not hold for the existential second-order sentences whose first-order part is in the godel prenex form with equality.>