[Back]

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 infinity
axioms and strengthened in that the space measure is relaxed to
ordered treewidth.

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