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→ 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.

websites: Arnold Beckmann 2017-08-28 Valid HTML 4.01! Valid CSS!