arnold beckmann's pages

Propositional Logic for Circuit Classes

File: PDF-File

Author: Klaus T Aehlig and Arnold Beckmann
Title: Propositional Logic for Circuit Classes
Proceedings: 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL,
Lausanne, Switzerland, September 11-15, 2007.
Pages: 512 - 526
DOI: 10.1007/978-3-540-74915-8_38

Abstract: By introducing a parallel extension rule that is aware of independence of the introduced extension variables, a calculus for quantified propositional logic is obtained where heights of derivations correspond to heights of appropriate circuits. Adding an uninterpreted predicate on bit-strings (analog to an oracle in relativised complexity classes) this statement can be made precise in the sense that the height of the most shallow proof that a circuit can be evaluated is, up to an additive constant, the height of that circuit.

The main tool for showing lower bounds on proof heights is a variant of an iteration principle studied by Takeuti. This reformulation might be of independent interest, as it allows for polynomial size formulae in the relativised language that require proofs of exponential height.

websites: Arnold Beckmann 2018-04-07 Valid HTML 4.01! Valid CSS!