Resolution refutations and propositional proofs with height-restriction

Abstract. Height restricted resolution (proofs or refutations) is a nat-ural restriction of resolution where the height of the corresponding proof tree is bounded. Height restricted resolution does not distinguish between tree- and sequence-like proofs. We show that polylogarithmic-height reso-lution is strongly connected to the bounded arithmetic theory S12(α). We separate polylogarithmic-height resolution from quasi-polynomial size tree-like resolution. Inspired by this we will study infinitely many sub-linear-height restric-tions given by functions n 7 → 2i (log(i+1) n)O(1) for i ≥ 0. We show that the resulting resolution systems are connected to certain bounded arithmetic theories, and that they form a strict hierarchy of resolution proof systems. To this end we will develop some proof theory for height restricted proofs