Pago, Benedikt
Finite Model Theory and Proof Complexity Revisited: Distinguishing Graphs in Choiceless Polynomial Time and the Extended Polynomial Calculus
Abstract
This paper extends prior work on the connections between logics from finite model theory and propositional/algebraic proof systems. We show that if all nonisomorphic graphs in a given graph class can be distinguished in the logic Choiceless Polynomial Time with counting (CPT), then they can also be distinguished in the boundeddegree extended polynomial calculus (EPC), and the refutations have roughly the same size as the resource consumption of the CPTsentence. This allows to transfer lower bounds for EPC to CPT and thus constitutes a new potential approach towards better understanding the limits of CPT. A superpolynomial EPC lower bound for a Ptimeinstance of the graph isomorphism problem would separate CPT from Ptime and thus solve a major open question in finite model theory. Further, using our result, we provide a model theoretic proof for the separation of boundeddegree polynomial calculus and boundeddegree extended polynomial calculus.
BibTeX  Entry
@InProceedings{pago:LIPIcs.CSL.2023.31,
author = {Pago, Benedikt},
title = {{Finite Model Theory and Proof Complexity Revisited: Distinguishing Graphs in Choiceless Polynomial Time and the Extended Polynomial Calculus}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {31:131:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959772648},
ISSN = {18688969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/17492},
URN = {urn:nbn:de:0030drops174923},
doi = {10.4230/LIPIcs.CSL.2023.31},
annote = {Keywords: finite model theory, proof complexity, graph isomorphism}
}
01.02.2023
Keywords: 

finite model theory, proof complexity, graph isomorphism 
Seminar: 

31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Issue date: 

2023 
Date of publication: 

01.02.2023 