Extended Frege proofs, circuits and rewriting

Abstract

Inspired by a statement about Extended Frege proof systems by Jain and Jin (FOCS 2022) we prove that: - there is a p-time binary relation $\approx$ between circuits that implies their logical equivalence, - if the equivalence $C\equiv D$ has an Extended Frege or a Circuit Frege proof with $k$ steps then there is a chain of circuits $E_i$ $$C=E_0\approx \cdots \approx E_t=D$$ with $t\le O(k\log k)$, and the total size of the chain is bounded above by $(k+|C|+|D|{)}^{O(1)}$.

arXiv commenta substantial revision, 11 pp