Resolution with Counting: Dag-Like Lower Bounds and Different Moduli

Fedor Part, Iddo Tzameret

Resolution over linear equations is a natural extension of the popular resolution refutation system, augmented with the ability to carry out basic counting. Denoted Res(lin_R), thi…