https://www.dagstuhl.de/21472

November 21 – 26 , 2021, Dagstuhl Seminar 21472

Geometric Logic, Constructivisation, and Automated Theorem Proving

Organizers

Thierry Coquand (University of Gothenburg, SE)
Hajime Ishihara (JAIST – Ishikawa, JP)
Sara Negri (University of Genova, IT)
Peter M. Schuster (University of Verona, IT)

For support, please contact

Dagstuhl Service Team

Documents

Dagstuhl Report, Volume 11, Issue 10 Dagstuhl Report
Aims & Scope
List of Participants
Shared Documents
Dagstuhl Seminar Schedule [pdf]

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.

Summary text license
  Creative Commons BY 4.0
  Thierry Coquand, Hajime Ishihara, Sara Negri, and Peter M. Schuster

Classification

  • Data Structures / Algorithms / Complexity
  • Semantics / Formal Methods
  • Verification / Logic

Keywords

  • Geometric logic
  • Constructivisation
  • Automated theorem proving
  • Proof theory
  • Categorical semantics

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.