TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 21472

Geometric Logic, Constructivisation, and Automated Theorem Proving

( Nov 21 – Nov 26, 2021 )


Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/21472

Organizers

Contact


Schedule

Motivation

Right at the origin of the development of the modern concepts of proof and computation, fundamental both to mathematics and computer science, Brouwer was advocating the exclusive use of effective methods of proof, designed intuitionism, whereas Hilbert was arguing that non-effective methods are important for the progress of mathematics, viewing constructivisation as an activity to take place after the fact. While the Brouwer–Hilbert debate arose from epistemological concerns about mathematics, the interplay between effective and non-effective proof has become more and more relevant since the advent of theoretical and actual computing devices: We now know that, to a certain extent, intuitionistic logic can be seen as the logic of computation.

A central question has remained from that discussion: What is the extent of intuitionistic mathematics? Ordinal analysis is an attempt to describe how strong subsystems of analysis can be proved consistent in intuitionistic mathematics. Another foundational solution, with the goal of rebuilding mathematics constructively, is aimed at by Bishop-style constructive mathematics and by Martin-Löf’s intuitionistic type theory, the latter most recently in the form of the so-called homotopy or univalent type theory put forward by Voevodsky.

From a more practical angle, the question rather is to which extent any given proof is effective, which proofs of which theorems can be rendered effective, and whether and how numerical information such as bounds and algorithms can be extracted from proofs. Ideally, all this is done by manipulating proofs mechanically and/or by adequate metatheorems (proof translations, automated theorem proving, program extraction from proofs, proof analysis, proof mining, etc.). In this vein, the central question should be put as follows: What is the computational content of proofs?

This Dagstuhl Seminar will be guided by this central question, putting a special focus on coherent and geometric theories and their generalisations: for they are (a) fairly widespread in mathematics and non-classical logics such as temporal and modal logics, (b) a priori amenable for constructivisation (Barr’s Theorem), and (c) particularly suited as a basis for automated theorem proving. Specific topics include (i) categorical semantics for geometric theories, (ii) complexity issues of and algorithms for geometrisation of theories including speed-up questions, (iii) the use of geometric theories in constructive mathematics including finding algorithms, (iv) proof-theoretic presentation of sheaf models and higher toposes and (v) coherent logic for obtaining automatically readable proofs.

Seminar presentations of recent research and refresher tutorials of ground knowledge will be complemented by parallel work groups on the relevant topics. Tutorials of two hours each are planned about proof theory of geometric logic, sheaf models and constructive algebra, proof mining and program extraction in axiomatic environments, and automated theorem proving with coherent logic.

Copyright Thierry Coquand, Hajime Ishihara, Sara Negri, and Peter M. Schuster

Summary

A central question has remained from the foundational crisis of mathematics about a century ago: What is the extent of intuitionistic mathematics? From a practical angle, the question is to which extent any given proof is effective, which proofs of which theorems can be rendered effective, and whether and how numerical information such as bounds and algorithms can be extracted from proofs. Ideally, all this is treated by manipulating proofs mechanically and/or by adequate proof-theoretic metatheorems (proof translations, automated theorem proving, program extraction from proofs, proof analysis, proof mining, etc.). In this vein, the central question should rather be put as follows: What is the computational content of proofs?

Guided by this form of the central question, the Dagstuhl Seminar 21472 put a special focus on coherent and geometric theories and their generalisations. These indeed are fairly widespread in mathematics and non-classical logics such as temporal and modal logics, a priori amenable for constructivisation in the vein of Barr's Theorem, and particularly suited as a basis for automated theorem proving. Specific topics included categorical semantics for geometric theories, complexity issues of and algorithms for geometrisation of theories with the related speed-up questions, the use of geometric theories in constructive mathematics up to finding algorithms, proof-theoretic presentation of sheaf models and higher toposes, and coherent logic for automated proving.

The Dagstuhl Seminar 21472 attracted researchers and practitioners from all over the world, including participants from various research areas in order to broaden the scope of the seminar and to create connections between communities. The seminar participants presented and discussed their research by means of programmed and ad-hoc talks, and a tutorial on Agda the well developed proof assistant based on dependent type theory - was held over several time slots. Numerous new research directions were developed in small working groups: for example, new perspectives on classifying toposes in algebraic geometry, applications of dynamical methods to quadratic forms, and Zorn induction to capture transfinite methods computationally.

The tireless efforts by Dagstuhl staff notwithstanding, it would not be fair to say that this seminar did not suffer from the pandemic-related travel restrictions by which many invitees were confined to remote participation, which of course made hard if not impossible that they took part at the invaluable informal exchange on-site characteristic for events held at Dagstuhl. Under the given circumstances, however, the seminar was still judged a success by all the participants. Following an unconditional request by many, the organisers intend to propose a follow-up Dagstuhl seminar on a related topic in the near future - if possible, all on-site.

Copyright Thierry Coquand, Hajime Ishihara, Sara Negri, and Peter M. Schuster

Participants
On-site
  • Karim Johannes Becher (University of Antwerp, BE)
  • Arnold Beckmann (Swansea University, GB) [dblp]
  • Ulrich Berger (Swansea University, GB) [dblp]
  • Ingo Blechschmidt (Universität Augsburg, DE)
  • Ulrik Buchholtz (TU Darmstadt, DE) [dblp]
  • Gabriele Buriola (University of Verona, IT)
  • Giulio Fellin (University of Verona, IT)
  • Anton Freund (TU Darmstadt, DE) [dblp]
  • Matthias Hutzler (Universität Augsburg, DE)
  • Rosalie Iemhoff (Utrecht University, NL) [dblp]
  • Ulrich Kohlenbach (TU Darmstadt, DE) [dblp]
  • Henri Lombardi (University of Franche-Comté - Besancon, FR) [dblp]
  • Julien Narboux (University of Strasbourg, FR) [dblp]
  • Stefan Neuwirth (University of Franche-Comté - Besancon, FR)
  • Eugenio Orlandelli (University of Bologna, IT) [dblp]
  • Iosif Petrakis (LMU München, DE)
  • Morgan Rogers (University of Insubria - Como, IT)
  • Peter M. Schuster (University of Verona, IT) [dblp]
  • Matteo Tesi (Scuola Normale Superiore - Pisa, IT)
Remote:
  • Jan Belle (LMU München, DE)
  • Marc Bezem (University of Bergen, NO)
  • Pierre Boutry (INRIA - Sophia Antipolis, FR) [dblp]
  • Olivia Caramello (University of Insubria - Como, IT)
  • Liron Cohen (Ben Gurion University - Beer Sheva, IL)
  • Thierry Coquand (University of Gothenburg, SE) [dblp]
  • Laura Crosilla (University of Oslo, NO)
  • Tiziano Dalmonte (University of Turin, IT) [dblp]
  • Makoto Fujiwara (Meiji University - Kawasaki, JP) [dblp]
  • Hajime Ishihara (JAIST - Ishikawa, JP) [dblp]
  • Predrag Janicic (University of Belgrade, RS) [dblp]
  • Tatsuji Kawai (JAIST - Nomi, JP) [dblp]
  • Vesna Marinkovic (University of Belgrade, RS) [dblp]
  • Kenju Miyamato (LMU München, DE)
  • Sara Negri (University of Genova, IT) [dblp]
  • Takako Nemoto (Hiroshima Institute of Technology, JP) [dblp]
  • Satoru Niki (Ruhr-Universität Bochum, DE)
  • Edi Pavlovic (LMU München, DE)
  • Cosimo Perini Brogi (University of Genova, IT)
  • Thomas Powell (University of Bath, GB) [dblp]
  • Michael Rathjen (University of Leeds, GB) [dblp]
  • Helmut Schwichtenberg (LMU München, DE) [dblp]
  • Monika Seisenberger (Swansea University, GB) [dblp]
  • Sana Stojanovic-Djurdjevic (University of Belgrade, RS) [dblp]
  • Daniel Wessel (LMU München, DE) [dblp]
  • Chuangjie Xu (fortiss GmbH - München, DE)

Related Seminars
  • Dagstuhl Seminar 24021: From Proofs to Computation in Geometric Logic and Generalizations (2024-01-07 - 2024-01-12) (Details)

Classification
  • data structures / algorithms / complexity
  • semantics / formal methods
  • verification / logic

Keywords
  • geometric logic
  • constructivisation
  • automated theorem proving
  • proof theory
  • categorical semantics