Grädel, Erich and Grohe, Martin and Pago, Benedikt and Pakusa, Wied - A Finite-Model-Theoretic View on Propositional Proof Complexity

lmcs:4320 - Logical Methods in Computer Science, January 23, 2019, Volume 15, Issue 1
A Finite-Model-Theoretic View on Propositional Proof Complexity

Authors: Grädel, Erich and Grohe, Martin and Pago, Benedikt and Pakusa, Wied

We establish new, and surprisingly tight, connections between propositional proof complexity and finite model theory. Specifically, we show that the power of several propositional proof systems, such as Horn resolution, bounded-width resolution, and the polynomial calculus of bounded degree, can be characterised in a precise sense by variants of fixed-point logics that are of fundamental importance in descriptive complexity theory. Our main results are that Horn resolution has the same expressive power as least fixed-point logic, that bounded-width resolution captures existential least fixed-point logic, and that the polynomial calculus with bounded degree over the rationals solves precisely the problems definable in fixed-point logic with counting. By exploring these connections further, we establish finite-model-theoretic tools for proving lower bounds for the polynomial calculus over the rationals and over finite fields.


Source : oai:arXiv.org:1802.09377
DOI : 10.23638/LMCS-15(1:4)2019
Volume: Volume 15, Issue 1
Published on: January 23, 2019
Submitted on: February 27, 2018
Keywords: Computer Science - Logic in Computer Science,F.4.1


Share