A Finite-Model-Theoretic View on Propositional Proof Complexity
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 monomial calculus of bounded degree, can be ch...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2022-06-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/4320/pdf |
| _version_ | 1797268562093539328 |
|---|---|
| author | Erich Grädel Martin Grohe Benedikt Pago Wied Pakusa |
| author_facet | Erich Grädel Martin Grohe Benedikt Pago Wied Pakusa |
| author_sort | Erich Grädel |
| collection | DOAJ |
| description | 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 monomial 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. We also study the
bounded-degree polynomial calculus. Over the rationals, it captures fixed-point
logic with counting if we restrict the bit-complexity of the coefficients. For
unrestricted coefficients, we can only say that the bounded-degree polynomial
calculus is at most as powerful as bounded variable infinitary counting logic,
but a precise logical characterisation of its power remains an open problem.
These connections between logics and proof systems allow us to establish
finite-model-theoretic tools for proving lower bounds for the polynomial
calculus over the rationals and also over finite fields.
This is a corrected version of the paper (arXiv:1802.09377) published
originally on January 23, 2019. |
| first_indexed | 2024-04-25T01:34:27Z |
| format | Article |
| id | doaj.art-6370b35ceda74a2cacae93fff8490101 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:27Z |
| publishDate | 2022-06-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-6370b35ceda74a2cacae93fff84901012024-03-08T10:27:56ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742022-06-01Volume 15, Issue 110.23638/LMCS-15(1:4)20194320A Finite-Model-Theoretic View on Propositional Proof ComplexityErich GrädelMartin GroheBenedikt PagoWied PakusaWe 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 monomial 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. We also study the bounded-degree polynomial calculus. Over the rationals, it captures fixed-point logic with counting if we restrict the bit-complexity of the coefficients. For unrestricted coefficients, we can only say that the bounded-degree polynomial calculus is at most as powerful as bounded variable infinitary counting logic, but a precise logical characterisation of its power remains an open problem. These connections between logics and proof systems allow us to establish finite-model-theoretic tools for proving lower bounds for the polynomial calculus over the rationals and also over finite fields. This is a corrected version of the paper (arXiv:1802.09377) published originally on January 23, 2019.https://lmcs.episciences.org/4320/pdfcomputer science - logic in computer sciencef.4.1 |
| spellingShingle | Erich Grädel Martin Grohe Benedikt Pago Wied Pakusa A Finite-Model-Theoretic View on Propositional Proof Complexity Logical Methods in Computer Science computer science - logic in computer science f.4.1 |
| title | A Finite-Model-Theoretic View on Propositional Proof Complexity |
| title_full | A Finite-Model-Theoretic View on Propositional Proof Complexity |
| title_fullStr | A Finite-Model-Theoretic View on Propositional Proof Complexity |
| title_full_unstemmed | A Finite-Model-Theoretic View on Propositional Proof Complexity |
| title_short | A Finite-Model-Theoretic View on Propositional Proof Complexity |
| title_sort | finite model theoretic view on propositional proof complexity |
| topic | computer science - logic in computer science f.4.1 |
| url | https://lmcs.episciences.org/4320/pdf |
| work_keys_str_mv | AT erichgradel afinitemodeltheoreticviewonpropositionalproofcomplexity AT martingrohe afinitemodeltheoreticviewonpropositionalproofcomplexity AT benediktpago afinitemodeltheoreticviewonpropositionalproofcomplexity AT wiedpakusa afinitemodeltheoreticviewonpropositionalproofcomplexity AT erichgradel finitemodeltheoreticviewonpropositionalproofcomplexity AT martingrohe finitemodeltheoreticviewonpropositionalproofcomplexity AT benediktpago finitemodeltheoreticviewonpropositionalproofcomplexity AT wiedpakusa finitemodeltheoreticviewonpropositionalproofcomplexity |