### 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.