Document Open Access Logo

Symmetric Proofs in the Ideal Proof System

Authors Anuj Dawar , Erich Grädel , Leon Kullmann, Benedikt Pago

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.MFCS.2025.40.pdf
  • Filesize: 0.84 MB
  • 18 pages
HTML5 Logo HTML (experimental)
LIPIcs.MFCS.2025.40.html

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Theory of computation → Algebraic complexity theory
  • Theory of computation → Finite Model Theory
Keywords
  • proof complexity
  • algebraic complexity
  • descriptive complexity
  • symmetric circuits
  • graph isomorphism

Metrics

Abstract

We consider the Ideal Proof System (IPS) introduced by Grochow and Pitassi and pose the question of which tautologies admit symmetric proofs, and of what complexity. The symmetry requirement in proofs is inspired by recent work establishing lower bounds in other symmetric models of computation. We link the existence of symmetric IPS proofs to the expressive power of logics such as fixed-point logic with counting and Choiceless Polynomial Time, specifically regarding the graph isomorphism problem. We identify relationships and tradeoffs between the symmetry of proofs and other parameters of IPS proofs such as size, degree and linearity. We study these on a number of standard families of tautologies from proof complexity and finite model theory such as the pigeonhole principle, the subset sum problem and the Cai-Fürer-Immerman graphs, exhibiting non-trivial upper bounds on the size of symmetric IPS proofs.

Cite As Get BibTex

Anuj Dawar, Erich Grädel, Leon Kullmann, and Benedikt Pago. Symmetric Proofs in the Ideal Proof System. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 40:1-40:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.MFCS.2025.40

Author Details

Anuj Dawar
  • Department of Computer Science and Technology, University of Cambridge, UK
Erich Grädel
  • Mathematical Foundations of Computer Science, RWTH Aachen University, Germany
Leon Kullmann
  • RWTH Aachen University, Germany
Benedikt Pago
  • Department of Computer Science and Technology, University of Cambridge, UK

Funding

  • Dawar, Anuj: Funded by UK Research and Innovation (UKRI) under the UK government’s Horizon Europe funding guarantee: grant number EP/X028259/1.
  • Pago, Benedikt: Funded by UK Research and Innovation (UKRI) under the UK government’s Horizon Europe funding guarantee: grant number EP/X028259/1.

Acknowledgements

We are grateful to Iddo Tzameret for familiarising us with the current trends in IPS lower bounds and for valuable suggestions for future directions of this project.

References

  1. Albert Atserias, Andrei Bulatov, and Anuj Dawar. Affine systems of equations and counting infinitary logic. Theoretical Computer Science, 410(18):1666-1683, 2009. URL: https://doi.org/10.1016/J.TCS.2008.12.049.
  2. Paul Beame and Toniann Pitassi. Propositional proof complexity: Past, present, and future. Current Trends in Theoretical Computer Science Entering the 21st Century, pages 42-70, 2001. Google Scholar
  3. Christoph Berkholz and Martin Grohe. Limitations of algebraic approaches to graph isomorphism testing. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming, pages 155-166, Berlin, Heidelberg, 2015. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-47672-7_13.
  4. Andreas Blass, Yuri Gurevich, and Saharon Shelah. Choiceless polynomial time. Annals of Pure and Applied Logic, 100(1):141-187, 1999. URL: https://doi.org/10.1016/S0168-0072(99)00005-6.
  5. Samuel R Buss. Polynomial size proofs of the propositional pigeonhole principle. The Journal of Symbolic Logic, 52(4):916-927, 1987. URL: https://doi.org/10.2307/2273826.
  6. J. Cai, M. Fürer, and N. Immerman. An optimal lower bound on the number of variables for graph identification. Combinatorica, 12:389-410, 1992. URL: https://doi.org/10.1007/BF01305232.
  7. Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the twenty-eighth annual ACM symposium on Theory of computing, pages 174-183, 1996. Google Scholar
  8. Anuj Dawar. The nature and power of fixed-point logic with counting. ACM SIGLOG News, 2(1):8-21, 2015. URL: https://doi.org/10.1145/2728816.2728820.
  9. Anuj Dawar. Symmetric computation (invited talk). In 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, 2020. URL: https://doi.org/10.4230/LIPIcs.CSL.2020.2.
  10. Anuj Dawar. Limits of symmetric computation (invited talk). In 51st International Colloquium on Automata, Languages, and Programming, ICALP 2024, volume 297 of LIPIcs, pages 1:1-1:8, 2024. URL: https://doi.org/10.4230/LIPICS.ICALP.2024.1.
  11. Anuj Dawar, Erich Grädel, Leon Kullmann, and Benedikt Pago. Symmetric Proofs in the Ideal Proof System, 2025. URL: https://doi.org/10.48550/arXiv.2504.16820.
  12. Anuj Dawar and Benedikt Pago. A logic for P: are we nearly there yet? ACM SIGLOG News, 11:35-60, 2024. URL: https://doi.org/10.1145/3665453.3665459.
  13. Anuj Dawar, Benedikt Pago, and Tim Seppelt. Symmetric algebraic circuits and homomorphism polynomials. arXiv, abs/2502.06740, 2025. URL: https://doi.org/10.48550/arXiv.2502.06740.
  14. Anuj Dawar, David Richerby, and Benjamin Rossman. Choiceless Polynomial Time, Counting and the Cai-Fürer-Immerman graphs. Annals of Pure and Applied Logic, 152(1-3):31-50, 2008. URL: https://doi.org/10.1016/J.APAL.2007.11.011.
  15. Anuj Dawar and Gregory Wilsenach. Symmetric Arithmetic Circuits. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020), volume 168 of LIPIcs, pages 36:1-36:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.36.
  16. Anuj Dawar and Gregory Wilsenach. Lower bounds for symmetric circuits for the determinant. In 13th Innovations in Theoretical Computer Science Conference, ITCS, volume 215 of LIPIcs, pages 52:1-52:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.ITCS.2022.52.
  17. Michael A. Forbes, Amir Shpilka, Iddo Tzameret, and Avi Wigderson. Proof Complexity Lower Bounds from Algebraic Circuit Complexity. In Ran Raz, editor, 31st Conference on Computational Complexity (CCC 2016), volume 50 of Leibniz International Proceedings in Informatics (LIPIcs), pages 32:1-32:17, Dagstuhl, Germany, 2016. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CCC.2016.32.
  18. Nashlen Govindasamy, Tuomas Hakoniemi, and Iddo Tzameret. Simple hard instances for low-depth algebraic proofs. In 2022 IEEE 63rd Annual Symposium on Foundations of Computer Science (FOCS), pages 188-199. IEEE, 2022. URL: https://doi.org/10.1109/FOCS54457.2022.00025.
  19. Erich Grädel and Martin Grohe. Is Polynomial Time Choiceless? In Fields of Logic and Computation II, pages 193-209. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-23534-9_11.
  20. Erich Grädel and Stefan Hegselmann. Counting in Team Semantics. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of Leibniz International Proceedings in Informatics (LIPIcs), pages 35:1-35:18, Dagstuhl, Germany, 2016. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.35.
  21. Joshua A. Grochow and Toniann Pitassi. Circuit Complexity, Proof Complexity, and Polynomial Identity Testing: The Ideal Proof System. J. ACM, 65(6), November 2018. URL: https://doi.org/10.1145/3230742.
  22. Armin Haken. The intractability of resolution. Theoretical computer science, 39:297-308, 1985. URL: https://doi.org/10.1016/0304-3975(85)90144-6.
  23. Tuomas Hakoniemi, Nutan Limaye, and Iddo Tzameret. Functional lower bounds in algebraic proofs: Symmetry, lifting, and barriers. In Proceedings of the 56th Annual ACM Symposium on Theory of Computing, pages 1396-1404, 2024. URL: https://doi.org/10.1145/3618260.3649616.
  24. Sandra Kiefer. The Weisfeiler-Leman algorithm: an exploration of its power. ACM SIGLOG News, 7(3):5-27, 2020. URL: https://doi.org/10.1145/3436980.3436982.
  25. Jan Krajíček. Proof Complexity, volume 170. Cambridge University Press, 2019. Google Scholar
  26. Martin Otto. Bounded Variable Logics and Counting, volume 9 of Lecture Notes in Logic. Springer, 1997. Google Scholar
  27. Benedikt Pago. Finite Model Theory and Proof Complexity Revisited: Distinguishing Graphs in Choiceless Polynomial Time and the Extended Polynomial Calculus. In Bartek Klin and Elaine Pimentel, editors, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), volume 252 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1-31:19, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.31.
  28. Wied Pakusa. Linear Equation Systems and the Search for a Logical Characterisation of Polynomial Time. PhD thesis, RWTH Aachen, 2015. Google Scholar
  29. Wied Pakusa, Benedikt Pago, Martin Grohe, and Erich Grädel. A Finite-Model-Theoretic View on Propositional Proof Complexity. Logical Methods in Computer Science, 15, 2019. URL: https://doi.org/10.23638/LMCS-15(1:4)2019.
  30. Alexander A Razborov. Lower bounds for the polynomial calculus. computational complexity, 7:291-324, 1998. URL: https://doi.org/10.1007/S000370050013.
  31. Benjamin Rossman. Choiceless Computation and Symmetry. In Fields of Logic and Computation, pages 565-580. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15025-8_28.
  32. Nathan Segerlind. The Complexity of Propositional Proofs. Bulletin of symbolic Logic, 13(4):417-481, 2007. URL: https://doi.org/10.2178/BSL/1203350879.
  33. Amir Shpilka and Avi Wigderson. Depth-3 arithmetic circuits over fields of characteristic zero. Computational Complexity, 10:1-27, 2001. URL: https://doi.org/10.1007/PL00001609.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact