[Proof Complexity] New preprint

[Theodoros Papamakarios]

Dear colleagues,

I am contacting you to let you know that a new preprint, "Space
characterizations of complexity measures and size-space trade-offs in
propositional proof systems", by Alexander Razborov and me, is available at

http://people.cs.uchicago.edu/%7Erazborov/files/small_space.pdf
https://people.cs.uchicago.edu/~papamakarios/spchv4.pdf

Abstract: We identify two new big clusters of proof complexity measures
equivalent up to polynomial and logn factors. The first cluster contains,
among others, the logarithm of tree-like resolution size, amortized (that
is, multiplied by the logarithm of proof length) clause and monomial space,
and clause space, both ordinary and amortized, in regular and tree-like
resolution. As a consequence, separating clause or monomial space from the
(logarithm of) tree-like resolution size is the same as showing a strong
trade-off between clause or monomial space and proof length, and is the
same as showing a super-critical trade-off between clause space and depth.
The second cluster contains width, Sigma2 space (a generalization of
clause space
to depth 2 Frege systems), both ordinary and amortized, as well as the
logarithm of tree-like size in the system R(log). As an application of some
of these simulations, we improve a known size-space trade-off for
polynomial calculus with resolution. In terms of lower bounds, we show
a quadratic
lower bound on tree-like resolution size for formulas refutable in clause
space 4. We introduce on our way yet another proof complexity measure
intermediate between depth and the logarithm of tree-like size that might
be of independent interest.

Suggestions and comments are most welcome!

Best,
Theodoros Papamakarios