Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472)

Authors Thierry Coquand, Hajime Ishihara, Sara Negri, Peter M. Schuster and all authors of the abstracts in this report

Thumbnail PDF


  • Filesize: 3.02 MB
  • 22 pages

Document Identifiers

Author Details

Thierry Coquand
  • University of Gothenburg, SE
Hajime Ishihara
  • JAIST - Ishikawa, JP
Sara Negri
  • University of Genova, IT
Peter M. Schuster
  • University of Verona, IT
and all authors of the abstracts in this report

Cite AsGet BibTex

Thierry Coquand, Hajime Ishihara, Sara Negri, and Peter M. Schuster. Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472). In Dagstuhl Reports, Volume 11, Issue 10, pp. 151-172, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


At least from a practical and contemporary angle, the time-honoured question about the extent of intuitionistic mathematics 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. All this is ideally done by manipulating proofs mechanically or by adequate metatheorems, which includes proof translations, automated theorem proving, program extraction from proofs, proof analysis and proof mining. The question should thus be put as: What is the computational content of proofs? Guided by this central question, the present Dagstuhl seminar puts a special focus on coherent and geometric theories and their generalisations. These are not only widespread in mathematics and non-classical logics such as temporal and modal logics, but also a priori amenable for constructivisation, e.g., by Barr’s Theorem, and last but not least particularly suited as a basis for automated theorem proving. Specific topics include categorical semantics for geometric theories, complexity issues of and algorithms for geometrisation of theories including speed-up questions, the use of geometric theories in constructive mathematics including finding algorithms, proof-theoretic presentation of sheaf models and higher toposes, and coherent logic for automatically readable proofs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
  • Theory of computation → Proof theory
  • Theory of computation → Automated reasoning
  • automated theorem proving
  • categorical semantics
  • constructivisation
  • geometric logic
  • proof theory


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads