Algebraic models of computation and interpolation for algebraic proof systems
Pavel Pudlák, Jiřı́ Sgall · DIMACS series in discrete mathematics and theoretical computer science · 1997
this paper we are interested in systems that use uses polynomials instead of boolean formulas. From the previous list this includes the Nullstellensatz refutations. Recently a stronger system using polynomials was proposed, the polynomial calculus, also called the Groebner calculus [9]. The proof systems form a similar hierarchy as the complexity classes or classes of circuits in the computational complexity, but there is no direct relation between the two hierarchies. Recently a new method was found which makes it possible to prove lower bounds on the length of proofs for some propositional proof systems using lower bounds on circuit complexity. This method is based on proving computationally efficient versions of Craig's interpolation theorem for the proof system in question [14, 18]. For appropriate tautologies the interpolation theorem