Séminaires du LIPN
Depuis 2007, plus de 1274 séminaires ont été présentés dans le laboratoire

Afficher les séminaires de

Séminaires passés
LOVE 23/05/2019 Towards a Combinatorial Proof Theory, par Ben Ralph
Ben Ralph, Inria Saclay  
Salle B107, bâtiment B, Université de Villetaneuse
23/05/2019    14:00 - 16:00
Résumé :
Combinatorial proofs have been introduced by Hughes to give a ``syntax-free'' presentations for proofs in classical propositional logic. In a nutshell, a classical combinatorial proof consists of two parts: (i) a linear part, and (ii) a skew fibration. The linear part encodes a proof in multiplicative linear logic (MLL), whose conclusion is given represented in a cograph, while the skew fibration maps this linear cograph to the cograph of the conclusion of the whole proof. For deep inference proofs, this skew fibration corresponds exactly to a contraction-weakening derivation. Applying certain restrictions to these two rules leads to substructural logics and substructural proof theory. These proof theoretic restrictions correspond precisely to set-theoretic and graph-theoretic restrictions on the skew fibration, allowing us to characterise proof systems by their graph homomorphism class.