Logic in Computer Science (LICS 2004)

Paper: Proof Nets and Boolean Circuits (at LICS 2004)

Authors: Kazushige Terui

Abstract

We study the relationship between proof nets for mutiplicative linear logic (with unbounded fan-in logical connectives) and Boolean circuits. We give simulations of each other in the style of the proofs-as-programs correspondence; proof nets correspond to Boolean circuits and cut-elimination corresponds to evaluation. The depth of a proof net is defined to be the maximum logical depth of cut formulas in it, and it is shown that every unbounded fan-in Boolean circuit of depth n, possibly with stCONN₂ gates, is polynomially simulated by a proof net of depth O(n) and vice versa. here, stCONN₂ stands for st-connectivity gates for undirected graphs of degree 2. Let APN{i} be the class of languages for which there is a polynomial size, log{i}-depth family of proof nets. We then have APN{i} = AC{i}(stCONN₂).

BibTeX

  @InProceedings{Terui-ProofNetsandBoolean,
    author = 	 {Kazushige Terui},
    title = 	 {Proof Nets and Boolean Circuits},
    booktitle =  {Proceedings of the Nineteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2004},
    year =	 2004,
    editor =	 {Harald Ganzinger},
    month =	 {July}, 
    pages =      {182--191},
    location =   {Turku, Finland}, 
    publisher =	 {IEEE Computer Society Press}
  }