All reports by Author Arnold Beckmann:

__
TR13-092
| 19th June 2013
__

Pavel Pudlak, Arnold Beckmann, Neil Thapen#### Parity Games and Propositional Proofs

Revisions: 1

__
TR03-034
| 17th March 2003
__

Arnold Beckmann#### Height restricted constant depth LK

Pavel Pudlak, Arnold Beckmann, Neil Thapen

A propositional proof system is \emph{weakly automatizable} if there

is a polynomial time algorithm which separates satisfiable formulas

from formulas which have a short refutation in the system, with

respect to a given length bound. We show that if the resolution

proof system is weakly automatizable, ...
more >>>

Arnold Beckmann

Height restricted constant depth LK is a natural restriction of

Gentzen's propositional proof system LK. A sequence of LK-formulas

has polylogarithmic-height restricted depth-d-LK proofs iff the

n-th formula in the sequence possesses LK-proofs where cut-formulas

are of depth d+1 with small bottom fanin

and of ...
more >>>