Question: Does anyone know of interesting applications of [Gröbner bases](http://en.wikipedia.org/wiki/Gr%C3%B6bner_basis) to theoretical computer science?

Gröbner bases are used to solve multi-variate polynomial equations, an NP-hard problem in general. I was wondering whether some tractable special cases were used to provide efficient algorithms/constructions/proofs in TCS or TCS-related areas (combinatorics, coding theory).

Answer: 
In proof complexity the use of Gröbner bases has been proposed by [Clegg, Edmonds, Impagliazzo](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.2402) to refute CNFs. There are cases in which this proof system outperforms Resolution exponentially but it does not seem to me that there is a real performance improvement for general instances. 

It is also true that many of the lower bounds for Resolution hold for Polynomial Calculus (a proof system based on Gröbner bases). The exceptions usually are built for the characteristic of the underlying field. This means that working in $GF(2)$ can help you on some formulas but not on others. 

Yet Polynomial Calculus has not been studied as much as Resolution, thus well tested heuristics are not available.

See also [this](http://martinralbrecht.files.wordpress.com/2010/10/phd.pdf) this for application in cryptanalysyis (I don't know very much about that).
Following <http://arxiv.org/pdf/1502.05912.pdf> sometimes grobner basis are used to decide isomorphism (when graphs are encoded by systems of equations). But this joins the use of grobner basis in refutating CNFS.