BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//wp-events-plugin.com//7.2.3.1//EN
TZID:Europe/Paris
X-WR-TIMEZONE:Europe/Paris
BEGIN:VEVENT
UID:8582@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20250227T110000
DTEND;TZID=Europe/Paris:20250227T123000
DTSTAMP:20250227T100908Z
URL:https://www.i2m.univ-amu.fr/evenements/graphes-existentiels-calcul-flo
 ral-theorie-des-topes-lsc/
SUMMARY:Pablo Donato (Istituto Grothendieck): Graphes existentiels\, calcul
  floral\, théorie des topes [LSC]
DESCRIPTION:Pablo Donato: Traditionnellement\, la théorie de la démonstra
 tion s'est établie comme une\nbranche de la logique symbolique: elle inca
 rne par excellence l'idéal\nhilbertien selon lequel tout concept mathéma
 tique peut être representé comme\nune suite finie de symboles\, le raiso
 nnement se réduisant alors à la\nmanipulation séquentielle de ces symbo
 les. Toutefois plusieurs évolutions\nrécentes tendent à démontrer qu'u
 ne analyse plus fine de la structure des\ndémonstrations est possible à 
 l'aide de représentations graphiques ou\ndiagrammatiques : on peut citer 
 les réseaux de preuves de Girard en logique\nlinéaire\, les diagrammes d
 e cordes en logique catégorique\, ou encore les\ncombinatorial proofs de 
 Hughes. L'idée est de s'abstraire de la séquentialité\narbitraire forc
 ée par les symboles\, en plongeant les preuves dans l'espace pour\nmieux 
 comprendre leur géométrie. Toutefois ces recherches se concentrent\nesse
 ntiellement sur la structure des démonstrations terminées\, en oubliant 
 le\nprocessus de manipulation séquentiel qui a permis leur construction. 
 Cela pose\nun obstacle à l'application de ces nouvelles méthodologies à
  la preuve assistée\npar ordinateur\, qui repose fondamentalement sur la 
 manipulation de\ndémonstrations partielles.\n\nPour résoudre ce problèm
 e\, nous explorons un formalisme diagrammatique oublié\ndes logiciens con
 temporains\, probablement car il prédate l'existence de la\nthéorie de l
 a démonstration : les graphes existentiels de C. S. Peirce.\nCelui-ci rep
 ose sur une représentation purement diagrammatique et topologique\ndes co
 nstantes logiques telles que la conjonction\, la négation et l'existence\
 ,\ninspirée d'une compréhension dialogique du raisonnement un siècle av
 ant\nl'avènement de la sémantique des jeux. La démonstration est alors 
 comprise\ncomme un processus dynamique de construction d'énoncés valides
  par réécriture\nde graphes\, à l'aide de quatre règles d'inférence 
 élémentaires par insertions\net omissions de graphes arbitraires.\n\nNou
 s commencerons par une présentation informelle des systèmes Alpha et Bet
 a de\ngraphes existentiels pour la logique classique propositionnelle et d
 u premier\nordre\, tels qu'introduits par Peirce en 1896. Puis\, motivés 
 par notre objectif\nd'application aux assistants de preuve\, nous concevon
 s le calcul floral\, une\nvariante intuitionniste de Beta basée sur la no
 tion de lieur où les graphes\napparaissent métaphoriquement sous forme d
 e fleurs. Pour modéliser plus\nfidèlement le processus de recherche de p
 reuve "en arrière"\, nous inversons le\nsens de lecture des règles d'inf
 érence\, ce qui nous permet d'identifier un\nfragment analytique et enti
 èrement réversible de règles via une sémantique de\npréfaisceaux (str
 uctures de Kripke). Forts de ces avancées\, nous nous éloignons\nde la c
 onception relationnelle de Peirce pour partir à la recherche d'une\ninter
 prétation computationnelle du calcul floral dans le style\nfonctionnel/BH
 K/Curry-Howard. Nous finirons l'exposé par une esquisse du\nnouveau terri
 toire ainsi approché et baptisé "théorie des topes"\, au sein\nduquel l
 a distinction entre un terme et son type se trouve mise en défaut.
CATEGORIES:Séminaire,Logique et Interactions
LOCATION:I2M Luminy - TPR2\, Salle de Séminaire 304-306 (3ème étage)\, 1
 63 Avenue de Luminy\, Marseille\, 13009\, France
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=163 Avenue de Luminy\, Mars
 eille\, 13009\, France;X-APPLE-RADIUS=100;X-TITLE=I2M Luminy - TPR2\, Sall
 e de Séminaire 304-306 (3ème étage):geo:0,0
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:STANDARD
DTSTART:20241027T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR