Affordable Access

Publisher Website

Separation results for the size of constant-depth propositional proofs

Authors
Journal
Annals of Pure and Applied Logic
0168-0072
Publisher
Elsevier
Publication Date
Volume
136
Identifiers
DOI: 10.1016/j.apal.2005.05.002
Keywords
  • Lengths Of Proofs
  • Propositional Calculus
  • Frege System
  • Ordering Principle

Abstract

Abstract This paper proves exponential separations between depth d -LK and depth ( d + 1 2 ) -LK for every d ∈ 1 2 N utilizing the order induction principle. As a consequence, we obtain an exponential separation between depth d -LK and depth ( d + 1 ) -LK for d ∈ N . We investigate the relationship between the sequence-size, tree-size and height of depth d -LK-derivations for d ∈ 1 2 N , and describe transformations between them. We define a general method to lift principles requiring exponential tree-size ( d + 1 2 ) -LK-refutations for d ∈ N to principles requiring exponential sequence-size d -LK-refutations, which will be described for the Ramsey principle and d = 0 . From this we also deduce width lower bounds for resolution refutations of the Ramsey principle.

There are no comments yet on this publication. Be the first to share your thoughts.