Sublogarithmic uniform Boolean proof nets

Journal article by Clément AubertORCID

Full text: Download

Publisher: Open Publishing Association

Preprint: policy unknown. Upload

Postprint: policy unknown. Upload

Published version: policy unknown. Upload

Policy details (opens in a new window). Data provided by SHERPA/RoMEO
Cut-elimination in proof nets for Multiplicative Linear Logic and evaluation in Boolean circuits may be linked using the proofs-as-programs correspondence. Those two models of parallel computation offer a framework where we can study uniformity and implicit complexity. Boolean proof nets were introduced by [Terui, 2004] and studied by [Mogbil & Rahli, 2007] to compare the computational power of proof nets and of Boolean circuits. They established inclusions between classes of complexity that could not be extended to sublogarithmic classes as AC0 and NC1. By restricting the way Boolean proof nets are built we prove anew those inclusion results -- in an uniform framework -- and extend them to small classes of complexity.