Coquand, Thierry ;
Ishihara, Hajime ;
Negri, Sara ;
Schuster, Peter M.
Weitere Beteiligte (Hrsg. etc.): Thierry Coquand and Hajime Ishihara and Sara Negri and Peter M. Schuster
Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472)
Abstract
At least from a practical and contemporary angle, the timehonoured 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 nonclassical 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 speedup questions, the use of geometric theories in constructive mathematics including finding algorithms, prooftheoretic presentation of sheaf models and higher toposes, and coherent logic for automatically readable proofs.
BibTeX  Entry
@Article{coquand_et_al:DagRep.11.10.151,
author = {Coquand, Thierry and Ishihara, Hajime and Negri, Sara and Schuster, Peter M.},
title = {{Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472)}},
pages = {151172},
journal = {Dagstuhl Reports},
ISSN = {21925283},
year = {2022},
volume = {11},
number = {10},
editor = {Coquand, Thierry and Ishihara, Hajime and Negri, Sara and Schuster, Peter M.},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/15932},
URN = {urn:nbn:de:0030drops159321},
doi = {10.4230/DagRep.11.10.151},
annote = {Keywords: automated theorem proving, categorical semantics, constructivisation, geometric logic, proof theory}
}
11.04.2022
Keywords: 

automated theorem proving, categorical semantics, constructivisation, geometric logic, proof theory 
Seminar: 

DagRep, Volume 11, Issue 10

Issue date: 

2022 
Date of publication: 

11.04.2022 