Localisation

Adresses

Aix-Marseille Université
Institut de Mathématiques de Marseille (I2M) - UMR 7373
Site Saint-Charles : 3 place Victor Hugo, Case 19, 13331 Marseille Cedex 3
Site Luminy : Campus de Luminy - Case 907 - 13288 Marseille Cedex 9

Séminaire

Combinatorial proofs for classical and intuitionistic logic [Lirica]

Lutz Straßburger
LIX, INRIA Saclay
https://www.lix.polytechnique.fr/~lutz/

Date(s) : 01/04/2025   iCal
10h00 - 11h30

(Séminaire de l’équipe Lirica au LIS)

Combinatorial proofs, or “proofs without syntax”, form a graphical
semantics of proof in various logics that is canonical yet
complexity-aware: they are a polynomial-sized representation
of sequent proofs that factors out exactly the non-duplicating
permutations. This is achieved by factoring a proof into a purely linear
proof and a resource management part.

In the talk, I will introduce combinatorial proofs for classical logic and
intuitionistic logic. And if time permits, I will also discuss their
normalization.

Emplacement
Luminy - LIS, salle 04.02

Catégories


Secured By miniOrange