arnold beckmann's pages
Resolution Refutations and Propositional Proofs
Author: Arnold Beckmann
Title: Resolution Refutations and Propositional Proofs
Proceedings: 16th International Workshop, CSL 2002,
Edinburgh, Scotland, UK, September 22-25, 2002
Pages: 599 - 612
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
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→ 2i((log(i+1) n)O(1))
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