Logic and interactions 2012

Proof circuits [Aubert, 11] are a clear and intuitive presentation of the Boolean proof nets [Terui, 04] in a uniform framework [Mogbil-Rahli, 07] : we define pieces as a set of links and edges of a unbounded variant of Multiplicative Linear Logic representing Boolean constants, n-ary disjunctions and conjonctions, negation and mechanisms such as deletion and duplication. Thoses pieces may be "plugged" together to obtain proof circuits : MLLu uniform Boolean proof nets whose size and depth are implicitly bounded and whose parralel normalization matches up evaluation in Boolean circuits. This light presentation allows sublogarithmic translation and simulation between Boolean circuits and proof circuits, lightens the size of the latter and preserves all the good properties concerning complexity. We conclude by giving the rst hints toward a full correspondence between proof circuits and alternating Turing machines, enlarging the correspondence between parallel models of computation.