Unsolvable systems of equations and proof complexity (Q1126839)

This is a survey of an algebraic approach to the efficiency of propositional proof systems. To a formula \(C\) in conjunctive normal form, one associates a set of polynomials \(Q_i\). (An atom \(p\) goes to \(1-y\), \(\neg p\) to \(y\), and \(\vee\) is replaced by \(x\). Thus each conjunct results in a polynomial. And, add \(y^2-y\) to confine the values to \(0\) and \(1\).) The given \(C\) is refutable iff the \(Q_i\)'s have no \(0/1\) solution iff, by the Nullstellensatz, \(\sum P_iQ_i= 1\) for some \(P_i\)'s. According to the author, ``Algebraic proof systems are appealing because of their simplicity and non-syntactic nature'' -- and, of course, much work has been done by algebraists on equations, the Nullstellensatz, etc. She compares algebraic proofs to Frege, resolution systems, etc., and talks about some methods and results (e.g., the design method, lower bounds for pigeonhole principles). The author gives good directions for future work by citing and commenting on open problems. We have also a recent good survey article by \textit{A. Urquhart} about ``The complexity of propositional proofs'' [Bull. Symb. Log. 1, No. 4, 425-467 (1995; Zbl 0845.03025)]. Compared to it, the present article is more research oriented in a narrowly focused area.