  We develop and study the complexity of propositional proof systems of varyingstrength extending resolution by allowing it to operate with disjunctions oflinear equations instead of clauses. We demonstrate polynomial-size refutationsfor hard tautologies like the pigeonhole principle, Tseitin graph tautologiesand the clique-coloring tautologies in these proof systems. Using the(monotone) interpolation by a communication game technique we establish anexponential-size lower bound on refutations in a certain, considerably strong,fragment of resolution over linear equations, as well as a general polynomialupper bound on (non-monotone) interpolants in this fragment.  We then apply these results to extend and improve previous results onmultilinear proofs (over fields of characteristic 0), as studied in[RazTzameret06]. Specifically, we show the following:  1. Proofs operating with depth-3 multilinear formulas polynomially simulate acertain, considerably strong, fragment of resolution over linear equations.  2. Proofs operating with depth-3 multilinear formulas admit polynomial-sizerefutations of the pigeonhole principle and Tseitin graph tautologies. Theformer improve over a previous result that established small multilinear proofsonly for the \emph{functional} pigeonhole principle. The latter are differentthan previous proofs, and apply to multilinear proofs of Tseitin mod p graphtautologies over any field of characteristic 0.  We conclude by connecting resolution over linear equations with extensions ofthe cutting planes proof system.
Using the (monotone) interpolation by a communication game technique we establish an exponential-size lower bound on refutations in a certain, considerably strong, fragment of resolution over linear equations, as well as a general polynomial upper bound on (non-monotone) interpolants in this fragment.