2026-07-22T12:31:26Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7689 2024-03-06T10:40:46Z ddc:004 open_access

The Model-Theoretic Expressiveness of Propositional Proof Systems Grädel, Erich Pago, Benedikt Pakusa, Wied Propositional proof systems fixed-point logics resolution polynomial calculus generalized quantifiers 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Erich Grädel and Benedikt Pago and Wied Pakusa 2017 Is Part Of LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2017.27 urn:nbn:de:0030-drops-76897 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.27 eng https://creativecommons.org/licenses/by/3.0/legalcode