Resolution augmented with the rule of symmetry or the rule of extension

Question

Krishnamurthy (here is the abstract of his paper) showed that resolution augmented with the principle of symmetry forms a proof system (referred to as SR) in which certain formulas (which do not admit short proof in resolution proof system) can exhibit short proofs.

This also holds for the resolution proof augmented with the rule of extension (referred to as ER). He however left open the question if these proof systems SR and ER p-simulate each other.

Is there any recent work on this question?

Does SR polynomially simulate ER?

Answer 1

First, ER p-simulates SR: for example, ER is p-equivalent to the extended Frege proof system (EF) which is p-equivalent to the substitution Frege proof system (SF), and it is easy to see that SF p-simulates SR (the symmetry rule amounts to substitution of a special kind).

On the other hand, Urquhart [1] proves an exponential lower bound on SR refutations of Tseitin tautologies for certain graphs. Since Tseitin formulas have polynomial-size ER (or extended Frege) refutations, this shows that ER is exponentially more powerful than SR.

Reference:

[1] Alasdair Urquhart: The symmetry rule in propositional logic, Discrete Applied Mathematics 96–97 (1999), pp. 177–193, doi: 10.1016/S0166-218X(99)00039-6.