<p>I found a <a href="https://mathweb.ucsd.edu/%7Esbuss/ResearchWeb/Caleidoscope/talkslides1.pdf" rel="nofollow noreferrer">slide</a> stating that &quot;extended resolution and extended Frege p-simulate each other&quot;, without providing a proof. It's obvious that extended Frege p-simulates extended resolution, but the converse is not so obvious. I've performed extensive search on how it works but found nothing. So, are there literature that explain this p-simulation in detail? Thanks!</p>

CC BY-SA 4.0
2023-04-28T06:44:49.910Z
See Krajicek "Proof complexity" (Encyc. Math. Appl., Cambridge Univ Press), Lemma 5.8.3. The key is "the construction underlying Lemma 2.4.6".
Joshua Grochow
CC BY-SA 4.0
2023-04-28T11:28:10.687Z
I thought this was in the Cook&Reckhow paper, but can’t find it there. Anyway, the simulation is rather simple: you introduce extension variables for all subformulas of all formulas in the EF proof. Then each application of a Frege rule is a valid inference from  $O(1)$ of these extension axioms, and therefore can be simulated by $O(1)$ resolution inferences.
Emil Jeřábek
<reference-request><proof-complexity><resolution>
How does extended resolution p-simulate extended Frege?
Soha
# How does extended resolution p-simulate extended Frege?

(Asked by: username_0 on 2023-04-28)

I found a [slide](https://mathweb.ucsd.edu/%7Esbuss/ResearchWeb/Caleidoscope/talkslides1.pdf) stating that "extended resolution and extended Frege p-simulate each other", without providing a proof. It's obvious that extended Frege p-simulates extended resolution, but the converse is not so obvious. I've performed extensive search on how it works but found nothing. So, are there literature that explain this p-simulation in detail? Thanks!

**Tags:** reference-request, proof-complexity, resolution
> **Comments:**
> **username_1**: See Krajicek "Proof complexity" (Encyc. Math. Appl., Cambridge Univ Press), Lemma 5.8.3. The key is "the construction underlying Lemma 2.4.6".  
> **username_2**: I thought this was in the Cook&Reckhow paper, but can’t find it there. Anyway, the simulation is rather simple: you introduce extension variables for all subformulas of all formulas in the EF proof. Then each application of a Frege rule is a valid inference from  $O(1)$ of these extension axioms, and therefore can be simulated by $O(1)$ resolution inferences.  

---

## 0 answers

