Extended Frege proofs, circuits and rewriting
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)}$.
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2606.13367
curl -X POST /api/v1/records/arxiv/2606.13367/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2606.13367/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'