摘要 : 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 VNC~1 (an extension of VNC_*~1), under the assumption of the existence of su... 展开 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 VNC~1 (an extension of VNC_*~1), 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 MLK. 收起