Automating Resolution is NP-Hard

Explore a comprehensive lecture on the complexity of automating resolution in propositional logic, presented by Albert Atserias and Moritz Müller at an IEEE conference. Delve into the historical context of the 2000s, understand the definition and examples of resolution, and examine the proof search problem. Investigate the proof system hierarchy, positive and negative results in the field, and a new construction technique. Learn about the reflection principle and its application to proof systems. Conclude with a recap of key concepts, lower boundary considerations, and engage with a quick question to reinforce understanding of this challenging topic in computational complexity theory.

Intro
Timeline
The 2000s
Defining Resolution
Resolution Example
Proof Search Problem
Proof System Hierarchy
Positive Results
Negative Results
New Construction
Reflection Principle
Proof System
Recap
Lower Boundary
Quick Question