Subscribe

Turku, Finland

July 17, 2004 to July 17, 2004

ISBN: 0-7695-2192-4

pp: 182-191

Kazushige Terui , National Institute of Informatics, Japan

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₂).

INDEX TERMS

null

CITATION

Kazushige Terui,
"Proof Nets and Boolean Circuits",

*LICS*, 2004, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science 2004, pp. 182-191, doi:10.1109/LICS.2004.1319612