SpringerLink - Book Chapter

Resolution Refutations and Propositional Proofs with Height-Restrictions

Book Series

Lecture Notes in Computer Science

Publisher

Springer Berlin / Heidelberg

ISSN

0302-9743 (Print) 1611-3349 (Online)

Volume

Volume 2471/2002

Book

Computer Science Logic

DOI

10.1007/3-540-45793-3

2002

ISBN

978-3-540-44240-0

DOI

10.1007/3-540-45793-3_40

Pages

375-396

Subject Collection

Computer Science

SpringerLink Date

Tuesday, January 01, 2002

Resolution Refutations and Propositional Proofs with Height-Restrictions

Arnold Beckmann⁵

(5)	Institute of Algebra and Computational Mathematics, Vienna University of Technology, Wiedner Hauptstr. 8-10/118, A-1040 Vienna, Austria

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 ₂ ¹ . 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⁽ⁱ⁺¹⁾ 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.

Keywords Height of proofs - Length of proofs - Resolution refutation - Propositional calculus - Frege systems - Order induction principle - Cut elimination - Cut introduction - Bounded arithmetic

MSC 03F20 - 03F07 - 68Q15 - 68R99

Supported by a Marie Curie Individual Fellowship #HPMF-CT-2000-00803 from the European Commission.

Arnold Beckmann
Email: arnold.beckmann@logic.at

Resolution Refutations and Propositional Proofs with Height-Restrictions

Fulltext Preview (Small, Large)