2026-07-20T14:36:13Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24147 2025-11-12T13:33:38Z ddc:004 open_access

Symmetric Proofs in the Ideal Proof System Dawar, Anuj Grädel, Erich Kullmann, Leon Pago, Benedikt proof complexity algebraic complexity descriptive complexity symmetric circuits graph isomorphism 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Anuj Dawar and Erich Grädel and Leon Kullmann and Benedikt Pago 2025 Is Part Of LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2025.40 urn:nbn:de:0030-drops-241477 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.40 eng https://creativecommons.org/licenses/by/4.0/legalcode