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...

Full description

Bibliographic Details
Main Authors: Erich Grädel, Martin Grohe, Benedikt Pago, Wied Pakusa
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