×

Uniform circuits, & Boolean proof nets. (English) Zbl 1132.03351

Artemov, Sergei N. (ed.) et al., Logical foundations of computer science. International symposium, LFCS 2007, New York, NY, USA, June 4–7, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72732-3/pbk). Lecture Notes in Computer Science 4514, 401-421 (2007).
Summary: The relationship between Boolean proof nets of multiplicative linear logic (APN) and Boolean circuits has been studied by K. Terui (2004) in a non-uniform setting. We refine this results by taking care of uniformity: the relationship can be expressed in term of the (Turing) polynomial hierarchy. We give a proofs-as-programs correspondence between proof nets and deterministic as well as non-deterministic Boolean circuits with a uniform depth-preserving simulation of each other. The Boolean proof nets class m&BN(poly) is built on multiplicative and additive linear logic with a polynomial amount of additive connectives as the non-deterministic circuit class NNC(poly) is with non-deterministic variables. We obtain uniform-\(\text{APN} = \text{NC}\) and \(\text{m\&BN(poly)} = \text{NNC(poly)} = \text{NP}\).
For the entire collection see [Zbl 1121.03005].

MSC:

03F52 Proof-theoretic aspects of linear logic and other substructural logics
03B70 Logic in computer science
03F07 Structure of proofs
68Q15 Complexity classes (hierarchies, relations among complexity classes, etc.)
94C10 Switching theory, application of Boolean algebra; Boolean functions (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI HAL