Parallel Time and Proof Complexity

Photograph of Klaus Aehlig

Klaus Aehlig

(Swansea University)

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.

An arithmetical formulation of the iteration principle yields a strength measure for theories in the language of relativised two-sorted Bounded Arithmetic. This measure provides all the separations Dynamic Ordinal Analysis provides, but extends to theories where the latter fails to produce any separation, due to the overhead of first-order (i.e., sharply-bounded) cut elimination. The new measure can also be used to investigate relativised theories for small complexity classes that are not necessarily based on restricted forms of induction. In particular, it can be used for theories that axiomatise computations, most prominently, deterministic and non-deterministic space computations, and the evaluation of circuits. Before studying relativised versions of these theories it is necessary to define relativised versions of the corresponding complexity classes. This can be done in such a way that the known inclusions are preserved.

Thursday 11th December 2008, 14:00
Robert Recorde Room
Department of Computer Science