Titre : Graph invariants in proof complexity
Exposant : Moritz Mueller
Résumé : 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 non-treelike ones.
Pathwidth and treewidth are well-known graph invariants. We introduce variations for directed graphs, called ordered pathwidth and ordered treewidth respectively. We are interested in the ordered treewidth or ordered pathwidth of the directed acyclic graphs underlying proofs, say, in Resolution. Roughly speaking, the ordered treewidth measures how close the proof is to be treelike, and the ordered pathwidth is related to its clause space. We generalize known time-space lower bounds in two ways, namely first by relaxing the usual clause space measure to ordered treewidth, and second by giving such lower bounds in general for infinity axioms. For example, the least number principle does not have short resolution refutations of bounded ordered treewidth.
This is joint work with Stefan Szeider.