<p>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).</p>

<p>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.</p>

<p><strong>Reference:</strong></p>

<p>[1] Alasdair Urquhart: <em>The symmetry rule in propositional logic</em>, Discrete Applied Mathematics 96–97 (1999), pp. 177–193, doi: <a href="https://doi.org/10.1016/S0166-218X(99)00039-6" rel="noreferrer">10.1016/S0166-218X(99)00039-6</a>.</p>

CC BY-SA 4.0
2018-08-14T14:02:57.153Z
2018-08-14T14:02:57.153Z
Emil Jeřábek
<p>Krishnamurthy (<a href="https://link.springer.com/article/10.1007%2FBF00265682" rel="nofollow noreferrer">here is the abstract of his paper</a>) 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.</p>

<p>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. </p>

<p>Is there any recent work on this question?</p>

<p>Does SR polynomially simulate ER?</p>

<sat><proof-complexity>
Resolution augmented with the rule of symmetry or the rule of extension
RTK
# Resolution augmented with the rule of symmetry or the rule of extension

(Asked by: username_0 on 2018-08-11)

Krishnamurthy ([here is the abstract of his paper](https://link.springer.com/article/10.1007%2FBF00265682)) 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?

**Tags:** sat, proof-complexity

---

## 1 answers

### Answer by username_1 on 2018-08-14. Score: 7 | Accepted answer

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](https://doi.org/10.1016/S0166-218X(99)00039-6).


---

