eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-08-16
27:1
27:18
10.4230/LIPIcs.CSL.2017.27
article
The Model-Theoretic Expressiveness of Propositional Proof Systems
Grädel, Erich
Pago, Benedikt
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 (monomial restriction of the) polynomial calculus of bounded degree solves precisely the problems definable in fixed-point logic with counting.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol082-csl2017/LIPIcs.CSL.2017.27/LIPIcs.CSL.2017.27.pdf
Propositional proof systems
fixed-point logics
resolution
polynomial calculus
generalized quantifiers