Graph invariants in proof complexity

Moritz Müller

An infinity axiom is a satisfiable first-order sentence without finite models. The fact that it does not have finite models can be expressed by a sequence of propositional contradictions, and it is an important issue to understand the proof complexity of these contradictions. For example, the least number principle does not have short treelike Resolution refutations, but does have short daglike ones.

We want to show that such short refutations of infinity axioms have to be complicated in some sense. Besides length, a popular complexity measure of Resolution refutations is clause space. We interpret clause space as a complexity measure concerning the dags underlying the proofs, namely as a natural version of pathwidth, which we call ordered pathwidth. We give a length-space lower bound for the corresponding notion of ordered treewidth and the R(k) refutation systems extending Resolution. This implies, for example, that short Resolution refutations of the least number principle need unbounded ordered treewidth; in this sense they are far from being treelike.

This is joint work with Stefan Szeider.

Back