Untitled

During the last two decades, an active line of research in proof complexity has been into the space complexity of proofs and how space is related to other measures.By now these aspects of the resolution proof system are fairly well understood, but many open problems remain for the related but stronger proof system polynomial calculus (PC/PCR).For instance, the space complexity of many standard "benchmark formulas" is still open, as well as the relation of space to size and degree in PC/PCR.We prove that if a formula requires large resolution width, then making XOR substitution yields a formula requiring large PCR space (and hence also PC space), providing some circumstantial evidence that degree might be a lower bound for