The theory of Groebner Bases, which has recently been
honored with the ACM Paris Kanellakis Theory and Practice Award,
has become a crucial building block to computer algebra, and is
widely used in science, engineering, and computer science. It is wellknown
that Groebner bases computation is EXP-SPACE in a general
polynomial ring setting.
However, for many important applications in computer science
such as satisfiability and automated verification of hardware and
software, computations are performed in a Boolean ring. In this paper,
we give an algorithm to show that Groebner bases computation is PSPACE
in Boolean rings. We also show that with this discovery,
the Groebner bases method can theoretically be as efficient as
other methods for automated verification of hardware and software.
Additionally, many useful and interesting properties of Groebner
bases including the ability to efficiently convert the bases for different
orders of variables making Groebner bases a promising method in
 G. S. Avrunin. Symbolic model checking using algebraic geometry. In
CAV -96: Proceedings of the 8th International Conference on Computer
Aided Verification, pages 26-37, London, UK, 1996. Springer-Verlag.
 A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic
model checking using SAT procedures instead of BDDs. In Proceedings
of Design Automation Conference (DAC-99), 1999.
 B. Buchberger. An Algorithm for Finding a Basis for the Residue Class
Ring of a Zero-dimensional Polynomial Ideal (in German). PhD thesis,
Institute of Mathematics, Univ. Innsbruck, Innsbruck, Austria, 1965.
 B. Buchberger. Groebner Bases: An algorithmic method in polynomial
ideal theory. In N. K. Bose, editor, Multidimensional Systems Theory,
chapter 6, pages 184-232. Reidel Publishing Company, Dodrecht, 1985.
 S. N. Burris and H. P. Sankappanavar. A Course in Universal Algebra.
 S. Collart, M. Kalkbrener, and D. Mall. Converting bases with the
Groebner walk. Journal of Symbolic Computation, 24(3/4):465-469,
 L. Csanky. Fast parallel matrix conversion algorithms. SIAM J. Comput.,
 N. Dershowitz, J. Hsiang, G. Huang, and D. Kaiss. Boolean ring
 N. Dershowitz, J. Hsiang, G. Huang, and D. Kaiss. Intersection-based
methods for satisfiability using boolean rings.
 T. D. Dub'e. The structure of polynomial ideals and Groebner bases.
SIAM J. Comput., 19(4):750-773, 1990.
 S. Fortune and J. Wyllie. Parallelism in random access machines.
In Proceedings of the 10th annual ACM symposium on Theory of
Computing, pages 114-118. ACM Press, 1978.
 Z. Galil and V. Pan. Parallel evaluation of the determinant and of the
inverse of a matrix. Inform. Proc. Lett., 30:41-45, 1989.
 G. Hermann. Die Frage der endlich vielen Schritte in der Theorie der
Polynomideale. Mathematische Annalen, 95:736-788, 1925.
 J. Hsiang. Refutational theorem proving using term rewriting systems.
Artificial Intelligence, 25:255-300, 1985.
 G. Huang, N. Dershowitz, and J. Hsiang. Satisfiability testing using
simplification in boolean rings.
 O. Ibarra, S. Moran, and L. Rosier. A note on the parallel complexity of
computing the rank of order n matrices. Inform. Proc. Lett, 11(4):162,
 D. Kaiss and N. Dershowitz. Boosting satisfiability testing using boolean
 K. Kuehnle and E. Mayr. Exponential space computation of groebner
bases. In Proceedings of ISSAC. ACM, 1996.
 O. Kupferman, M. Vardi, and P. Wolper. An automata-theoretic approach
to branching-time model checking. Journal of the ACM, 47(2):312-360,
 K. L. McMillan. Symbolic Model Checking. Kluwer Academic
 F. Preparata and D. Sarwata. An improved parallel processor bound in
fast matrix inversion. Inform. Proc. Lett., 1978.
 M. Sipser. Introduction to the Theory of Computation. PWS Publishing,
Boston, 2nd edition, 1997.
 M. Sipser. Introduction to the Theory of Computation. Course
Technology, 2nd edition, 2005.
 M. Stone. The theory of representation for boolean algebras. Trans.
Amer. Math. Soc., 1936.
 M. Stone. Applications of the theory of boolean rings to general
topology. Trans. Amer. Math. Soc., 1937.
 Q.-N. Tran. A fast algorithm for Groebner basis conversion and its
applications. Journal of Symbolic Computation, 30:451-468, 2000.
 Q.-N. Tran. A new class of term orders for elimination and applications.
Journal of Symbolic Computation, 42, 2007.
 Q.-N. Tran and M. Y. Vardi. Groebner bases computation in boolean
rings for symbolic model checking. In Proceedings of IASTED 2007
Conference on Modeling and Simulation, 2007.
 F. Winkler. Polynomial Algorithms in Computer Algebra. Texts and
Monographs in Symbolic Computation. Springer-Verlag, 1996.