Abstract:
In this talk we discuss sequent systems extending multiplicative linear logic with connectives allowing us to encode graphs with formulas with linear size with respect to the number of vertices of a graph.
We show that these systems satisfy basic proof theoretical properties such as initial coherence, cut-elimination and analyticity of proof search, therefore providing conservative extensions of multiplicative linear logic with and without mix.
We then provide proof nets for these logics together with correctness criteria and a sequentialization procedure..
Il seminario si svolgerà in presenza presso il Dipartimento di Matematica e Fisica,
Largo San Leonardo Murialdo,1- Aula 311.
This post is also available in:
Link identifier #identifier__69296-5
Eng