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: | 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 |
Similar Items
-
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
by: Robert Constable, et al.
Published: (2008-09-01) -
The Completeness of Propositional Resolution: A Simple and Constructive Proof
by: Jean Gallier
Published: (2006-11-01) -
Validity and Entailment in Modal and Propositional Dependence Logics
by: Miika Hannula
Published: (2019-04-01) -
Randomisation and Derandomisation in Descriptive Complexity Theory
by: Kord Eickmeyer, et al.
Published: (2011-09-01) -
The succinctness of first-order logic on linear orders
by: Martin Grohe, et al.
Published: (2005-06-01)