Lower bounds on Nullstellensatz proofs via designs
Samuel R. Buss · DIMACS series in discrete mathematics and theoretical computer science · 1997
. The Nullstellensatz proof system is a proof system for propositional logic based on algebraic identities in fields. Prior work has proved lower bounds of the degree Nullstellensatz refutations using combinatorial constructions called designs. This paper surveys the use of designs for Nullstellensatz lower bounds. We give a new, more general definition of designs. We present an explicit construction of designs which give a linear lower bound on the degree of Nullstellensatz proofs of the housesitting principle. Our designs for the housesitting principle work over any ring. 1. Introduction The Nullstellensatz proof system is a propositional proof system which establishes the truth of tautologies using reasoning about polynomials over a field, based on the Hilbert Nullstellensatz. The original definition of the Nullstellensatz proof system was by [2]. and many of the basic properties of Nullstellensatz proofs can be found in [3] and in the survey [6]. We begin with a review of...