11--12 July 2024

Logic at the Interface: Modal Logic and AI

University of Montpellier, France

Intro

Modal logic plays an important role in a number of different disciplines, including Computer Science and Artificial Intelligence. This workshop was developed as part of a BayFrance project between the University of Montpellier and the University of Bamberg. It focuses on recent work in the proof theory and modal theory of modal logic, and it particularly encourages the participation of students.

Attendance to the workshop is free, but please register at forms.gle/gs3WSBfy9VuWkNNL7 at least 1 week in advance.

Speakers

Lutz Strassburger

Lutz Strassburger is directeur de recherche at Inria Research Centre Saclay and head of the Partout team. His research interests include proof theory, logic programming, functional programming, software verification and category theory.

Eugenio Orlandelli

Eugenio Orlandelli is Associate Professor at the Department of the Arts at the University of Bologna. His principal research interests include quantified modal logic and its proof theory.

Sophie Pinchinat

Sophie Pinchinat is Full Professor at the University of Rennes at ISTIC (Department of Electrical Engineering and Computer Science) and a Research Scientist in the LogicA research team at IRISA / INRIA. Her principal research interests are Logic, Automata and Games, Formal methods for security and Diagnosis and Control Theory.

Stanislav Speranski

Stanislav Speranski is Senior Scientific Researcher at the Department of Mathematical Logic at Steklov Mathematical Institute. His work addresses topics in logic and computability, as well as problems in the foundations and philosophy of mathematics and computing. Among other things, he is concerned with the semantic, computational and proof-theoretic aspects of probability logic and various non-classical logics.

Tommaso Moraschini

Tommaso Moraschini is an Associate Professor at the Philosophy Department of the University of Barcelona (UB) and a member of the Institute of Mathematics of the UB. His research interests include Algebraic Logic, Duality Theory, Universal Algebra, and their applications to Intuitionistic and Modal Logics.

Tadeusz Litak

Tadeusz Litak is Akademischer Oberrat auf Zeit in Theoretical Computer Science at the Friedrich-Alexander-Universität Erlangen-Nürnberg. His principal research interests lie in constructive and/or modal logics, in particular their (co)algebraic semantics and CS applications.

Matteo Acclavio

Matteo Acclavio is Lecturer in Computer Science at the FoSS group of the University of Sussex. His principal research interests include proof theory, including the proof theory of modal logic and game semantics. He is also interested in applications of proof theory and in the didactics of mathematics and computer science.

Schedule

Thursday 11.07

09h00 -- 09h30 : Welcome + Coffee

09h30 -- 10h20 : Tommaso Moraschini - Intuitionistic Sahlqvist theory for deductive systems

10h20 -- 11h10 : Matteo Acclavio - Proof equivalence and denotational semantics of constructive modal logic

11h10 -- 11h40 : Discussion + Coffee

11h40 -- 12h30 : Lutz Straßburger - A Decision Algorithm for Intuitionistic S4

12h30 -- 14h30 : Lunch + coffee

14h30 -- 15h20 : Eugenio Orlandelli - Nested sequents for quantified modal logics with definite descriptions

15h20 -- 17h00 : Discussion + Student session

Friday 12.07

09h00 -- 09h30 : Coffee

09h30 -- 10h20 : Sophie Pinchinat - Strategic reasoning under imperfect information in the dynamic epistemic logic setting

10h20 -- 11h10 : Stanislav Speranski - Negation as a modality in a quantified setting

11h10 -- 11h40 : Discussion + Coffee

11h40 -- 12h30 : Tadeusz Litak - Lewis meets Brouwer: A Quick Overview of Constructive Strict Implication

12h30 -- 14h30 : Lunch + coffee

14h30 -- 16h10 : Discussion + Student session

16h10 -- 16h30 : Wrap-up

Venue

University of Montpellier

Montpellier, France

Our workshop will be held at the Faculté de Droit et de Science politique de Montpellier, Bâtiment 2, Rez-de-chaussée, Salle 02 (see map below).

The venue is located about 350m from tram station "Place Albert 1 Saint-Charles", served by (blue) line 1 and (brown) line 4, and 150m from tram station "Albert 1er - Cathédrale", served by line 4.

Organizers

Michael Mendler

Michael Mendler is head of the Informatics Theory Group, at the University of Bamberg. His principal research interests include Intuitionistic and constructive modal logics, Logical game theory, Process algebras and calculi for synchrony and asynchrony and Functional Programming Languages.

Christian Retoré

Christian Retoré is Professeur, Université de Montpellier at Equipe TEXTE, LIRMM and Coordinateur de l'axe transverse "logiques". His principal research interests include the proof and model theory of Intuitionistic Logic, Linear Logic and the Lambek calculus, and their applications in linguistics and elsewhere.

Luke Burke

Luke is a postdoctoral researcher in the theory group of the Information Systems and Applied Computer Science department of the University of Bamberg in Germany. He is interested in logic, types and monads, and their applications to natural language semantics and linguistics.

Michael Sioutis

Michael Sioutis is a Junior Professor with the LIRMM UMR 5506 laboratory and the Department of Computer Science of the University of Montpellier in France. His general interests lie in Hybrid Artificial Intelligence, Spatio-Temporal Reasoning, Data Mining, Semantic Web, Constraint Programming, and Logic.