Séminaires : Séminaire Général de Logique

Equipe(s) : lm,
Responsables :S. Anscombe, A. Khélif, A. Vignati
Email des responsables : sylvy.anscombe@imj-prg.fr, vignati@imj-prg.fr
Salle : 1013
Adresse :Sophie Germain

ArchivesRetour ligne automatique
Abonnement à la liste de diffusion

Orateur(s) Elaine Pimentel - UFRN, Brésil,
Titre A Game Model for Proofs with Costs (or: Trying to understand resource consciousness)
Horaire16:00 à 17:15
Diffusion https://u-paris.zoom.us/rec/share/CkyDTrmCUlxpybILW3Y_XqdQkoFflEUqNIXFuoWK7eAWIkEZDJKDqYUentVSXqSP.wj6WTn8kZIyiDnRr
RésumeWe look at substructural calculi from a game semantic point of view, guided by certain intuitions about resource conscious and, more specifically, cost conscious reasoning. To this aim, we start with a game, where player I defends a claim corresponding to a (single-conclusion) sequent, while player II tries to refute that claim. Branching rules for additive connectives are modeled by choices of II, while branching for multiplicative connectives leads to splitting the game into parallel subgames, all of which have to be won by player I to succeed. The game comes into full swing by adding cost labels to assumptions, and a corresponding budget. Different proofs of the same end-sequent are interpreted as more or less expensive strategies for I to defend the corresponding claim. This leads to a new kind of labelled calculus, which can be seen as a fragment of SELL (subexponential linear logic). Finally, we generalize the concept of costs in proofs by using a semiring structure, illustrate our interpretation by examples and investigate some proof-theoretical properties. The talk assumes *no prior knowledge* on games or substructural logic. Only a basic notion of sequent systems is advisable. This is a joint work with Timo Lang, Carlos Olarte and Christian G. Fermüller.
AdresseSophie Germain