[logic-ml] Talk by Marc Bagnol (9 Feb 11:00-)

[Tetsuya Sato]

京都大学数理解析研究所の佐藤です。

2月9日11:00から、東京大学のMarc Bagnol氏に
以下の講演をしていただくことになりましたので、
ご連絡いたします。どうぞお気軽にお越しください。
==========
Time:	11:00-12:00, 9 Feb, 2017
Place:	Rm 478, Research Building 2, Main Campus, Kyoto University
	京都大学 本部構内 総合研究2号館 4階478号室
	http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (Building 34)
	http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物)

Speaker: Marc Bagnol (JSPS Postdoctoral Fellow, University of Tokyo)

Title:	Multiplicative-Additive Proof Equivalence is Logspace-complete

Abstract:
Given a logic presented in a sequent calculus, a natural
question is that of equivalence of proofs: to determine
whether two given proofs are equated by any denotational
semantics, i.e. any categorical interpretation of the
logic compatible with its cut-elimination procedure. This
notion can usually be captured syntactically by a set of
rule permutations.

Very generally, proofnets can be defined as combinatorial
objects which provide canonical representatives of
equivalence classes of proofs. In particular, the existence
of proof nets for a logic provides a solution to the
equivalence problem of this logic. In certain fragments of
linear logic, it is possible to give a notion of proofnet
with good computational properties, making it a suitable
representation of proofs for studying the cut-elimination
procedure, among other things.

It has recently been proved that there cannot be such a
notion of proofnets for the multiplicative (with units) fragment
of linear logic, due to the equivalence problem for this
logic being Pspace-complete.

We will investigate the multiplicative-additive (without unit)
fragment of linear logic and see it is closely related to
binary decision trees: we can build a representation of proofs
based on binary decision trees, reducing proof equivalence to
decision tree equivalence. We will see as a consequence that
the proof equivalence problem multiplicative-additive linear
logic is Logspace-complete.