Dagstuhl Seminar on Geometric Logic, Constructivisation, and Automated Theorem Proving

21 - 26 Nov 2021Add To Calendar
Dagstuhl, Wadern, Germany
AboutFollowersReviewsExhibitorsPhotosSpeakersTravel Deals

A central question has remained from that discussion: What is the extent of intuitionistic mathematics? 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 .. continue reading 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. 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.


09:00 AM-06:00 PM (expected)
Not Verified

Entry Fees

Check Official Website


upto 100
Based on previous editions

Category & Type

Education & Training


Nov 2021 Interested
+1 more edition

Frequency Annual

Official Links


Report Error
Claim this event
Event Happening Alongside


LogoSend Stall Book Request

Leibniz-Institute for New Materials

Germany76 Total Events / 61 Upcoming Events

Write a Review

Add Your Review

Venue Map & Directions

map of Dagstuhl


Oktavie-Allee, 66687 Wadern, Germany

Get Directions

Featured Hotels in Wadern

More Hotels

You have no contacts. Please add contacts from below or share on social media

Send to all
No Results