Resolution with Symmetry Rule applied to Linear Equations

Pascal Schweitzer, Constantin Seebach

This paper considers the length of resolution proofs when using Krishnamurthy's classic symmetry rules. We show that inconsistent linear equation systems of bounded width over a fi…