All reports by Author Zhengyu Wang:

__
TR15-134
| 19th August 2015
__

Fu Li, Iddo Tzameret, Zhengyu Wang#### Characterizing Propositional Proofs as Non-Commutative Formulas

Fu Li, Iddo Tzameret, Zhengyu Wang

Does every Boolean tautology have a short propositional-calculus proof? Here, a propositional-calculus (i.e., Frege) proof is any proof starting from a set of axioms and deriving new Boolean formulas using a fixed set of sound derivation rules. Establishing any super-polynomial size lower bound on Frege proofs (in terms of the ... more >>>