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

## Documents

Dagstuhl Report, Volume 11, Issue 10

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