Interactions Between Proof Complexity and Finite Model Theory (part 2)

ABSTRACT. The main object of study in proof complexity are formal proofs of the unsatisfiability of propositional formulas, whereas finite model theory focuses on the expressibility and complexity of logics on finite structures. Although their research objects are different, several connections between both areas have been unveiled and techniques from one area have been fruitfully applied to make progress in the other. In this tutorial, I will give an introduction to propositional proof complexity, discuss some of the connections to finite model theory that have been established so far, and present results that have been obtained using these interactions.

Authors

• Christoph Berkholz

Keywords

No keywords are indexed for this paper.