### arnold beckmann's pages

## Resolution Refutations and Propositional Proofs
with Height-Restrictions

**File:** PDF-File

**Author:** Arnold Beckmann

**Title:** Resolution Refutations and Propositional Proofs
with Height-Restrictions

**Proceedings:** 16th International Workshop, CSL 2002,
Edinburgh, Scotland, UK, September 22-25, 2002

**Pages:** 599 - 612

**DOI:** 10.1007/3-540-45793-3_40

**Abstract:**
Height restricted resolution (proofs or refutations) is a natural
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 resolution is strongly
connected to the bounded arithmetic theory
S
1
2
(α)
.
We separate polylogarithmic-height resolution from
quasi-polynomial size tree-like resolution.

Inspired by this we will study infinitely many sub-linear-height
restrictions given by functions
n→ 2_{i}((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.