Skip to content
DraconiticResearch
Search Sources API
190,839 studies31 sourcesUpdated 4 min ago
PreprintCC BY 4.0arXiv

Extended Frege proofs, circuits and rewriting

  • Jan Krajicek
Open at sourcePDFDOICite

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 ≈ between circuits that implies their logical equivalence, - if the equivalence C ≡ D has an Extended Frege or a Circuit Frege proof with k steps then there is a chain of circuits Ei C = E0 ≈ … ≈ Et = D with t ≤ O(k log k), and the total size of the chain is bounded above by (k+|C|+|D|)O(1).

Related

  1. Exponential Gaps Between Intuitionistic Linear Extended Frege Systems
    Amirhossein Akbar Tabatabai
    arXivPreprintCC BY 4.0Full textLogic & foundationsarXiv
  2. Pseudo-solutions of polynomial systems and the lower bound problem for AC0[p]-Frege systems
    Jan Krajicek
    arXivPreprintCC BY 4.0Full textLogic & foundationsarXiv
  3. The tableaux monoid: a rewriting-theoretic approach
    Nohra Hage
    arXivPreprintCC BY-NC-SA 4.0Full textAlgebra & number theoryCombinatorics & discrete mathematicsarXiv
  4. Coherent presentations for stylic monoids via row rewriting
    Nohra Hage
    arXivPreprintCC BY-NC-SA 4.0Full textAlgebra & number theoryCombinatorics & discrete mathematicsarXiv
  5. Causal graph rewriting
    Pablo Arrighi, Marin Costes, Luidnel Maignan
    arXivPreprintCC BY 4.0Full textDynamical systemsMathematical physicsarXiv

Cite

BibTeXRIS
BibTeX
@misc{krajicek2026extended,
  title = {{Extended Frege proofs, circuits and rewriting}},
  author = {Jan Krajicek},
  howpublished = {arXiv},
  year = {2026},
  month = oct,
  doi = {10.48550/arxiv.2606.13367},
  eprint = {2606.13367},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2606.13367},
  note = {CC BY 4.0},
}
RIS
TY  - UNPB
TI  - Extended Frege proofs, circuits and rewriting
AU  - Jan Krajicek
PY  - 2026
DA  - 2026/10/15
PB  - arXiv
DO  - 10.48550/arxiv.2606.13367
UR  - https://arxiv.org/abs/2606.13367
AB  - 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 ≈ between circuits that implies their logical equivalence, - if the equivalence C ≡ 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 ≈ … ≈ E_t = D with t ≤ O(k log k), and the total size of the chain is bounded above by (k+|C|+|D|)^O(1).
ER  -