A sorting network in bounded arithmetic

13 years 1 months ago
A sorting network in bounded arithmetic
We formalize the construction of Paterson’s variant of the Ajtai–Koml´os–Szemer´edi sorting network of logarithmic depth in the bounded arithmetical theory VNC1 ∗ (an extension of VNC1 ), under the assumption of existence of suitable expander graphs. We derive a conditional p-simulation of the propositional sequent calculus in the monotone sequent calculus MLK.
Emil Jerábek
Added 12 May 2011
Updated 12 May 2011
Type Journal
Year 2011
Where APAL
Authors Emil Jerábek
Comments (0)