{"id":"arxiv/2606.13367","url":"https://arxiv.org/abs/2606.13367","tags":["math.LO","cs.CC"],"score":0,"title":"Extended Frege proofs, circuits and rewriting","domain":"math.LO","source":"arxiv","authors":["Jan Krajicek"],"reviews":0,"subject":"math.LO","summary":"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 \\dots \\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)}$.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-06-11","reactions":{}}