| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 4662620 | Annals of Pure and Applied Logic | 2011 | 15 Pages |
Abstract
We formalize the construction of Paterson’s variant of the Ajtai–Komlós–Szemerédi sorting network of logarithmic depth in the bounded arithmetical theory (an extension of ), under the assumption of the existence of suitable expander graphs. We derive a conditional p-simulation of the propositional sequent calculus in the monotone sequent calculus .
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
