Resolution Proof System and Graph Complexity

Alexander Knop

Goedel defined the first formal proof system at the beginning of the twentieth century. However, up until now, it is not clear how to generate proofs in this proof system efficiently. To overcome this obstacle, Davis and Putnam, in 1960, proposed resolution proof system, a much weaker proof system that allows generating proofs automatically.

In this talk, we define resolution proof system, discuss lower bounds for it, and give a graph theoretic open questions connected to these lower bounds.