M. Müller, S. Szeider:

"The Treewidth of Proofs";

Information and Computation,255(2017), 147 - 164.

So-called ordered variants of the classical notions of pathwidth and

treewidth are introduced and proposed as proof theoretically

meaningful complexity measures for the directed acyclic graphs

underlying proofs. Ordered pathwidth is roughly the same as proof

space and the ordered treewidth of a proof is meant to serve as a

measure of how far it is from being treelike. Length-space lower

bounds for k-DNF refutations are generalized to arbitrary inﬁnity

axioms and strengthened in that the space measure is relaxed to

ordered treewidth.

http://www.sciencedirect.com/science/article/pii/S0890540117300986?via%3Dihub

Created from the Publication Database of the Vienna University of Technology.