Naproche - Seminar on Formal Mathematics 2007

Organized by Peter Koepke, Grigori Mints, and Bernhard Schröder.

Thursday, March 22, 10:00-12:00, MPI (joint session with the Trimestre on Methods of Proof Theory in Mathematics):
Peter Koepke, The Language of Proofs (Slides)
Abstract: Proof theory treats mathematical proofs as formal proofs which proceed by syntactic manipulations of sequences of symbols. To the human reader proofs rather appear as tales about numbers, figures and other mathematical objects. We discuss whether standard linguistic techniques for the understanding of simple discourse are able to generate formal proofs from natural language proofs. This work may lead to natural interfaces for proof-checkers and provers and to a better understanding of the natural language and logic used in mathematical discourse. See also http://www.math.uni-bonn.de/people/naproche

Wednesday, March 28 17:00-19:00, MPI:
Technical Discussion of Naproche

Tuesday, April 3, 13:00-15:00, MPI:
Grigori Mints, Stanford, Advanced tools in computerized logic education
Abstract: An overview of computerized exercises developed for teaching definability and related notions in a course of first order logic at Stanford University

Tuesday, April 10, 13:00-15:00, MPI:
Bernhard Schröder, Dynamic aspects of the semantics of semi-formal proofs
Abstract: Like everyday language the language of semi-formal proofs exhibits a lot of phenomena, as e.g. anaphora and the interaction of quantifying expressions and implications, which can best be described in the framework of dynamic semantics. The talk will give a brief overview over dynamic-semantic approaches like Discourse Representation Theory (DRT) and Dynamic Predicate Logic (DPL), their motivation, and their basis in dynamic logic. Some dynamic-semantic phenomena are quite rare in everyday language, but pervasive in mathematics, like hypothetical propositions. Others, as the interaction of quantifying and anaphorical expressions with variables and other formal means of notation, are rather uniquely used in mathematics. Therefore, so far, natural language semantics has neglected them widely. The talk will try to fill parts of this gap.

Tuesday, April 17, 13:00-15:00, MPI:
Freek Wiedijk, Nijmegen, Readable formalization of mathematics.

Tuesday, April 24, 13:00-15:00, MPI:
Jesse Alama, Stanford, Formalizing Euler's Polyhedron Formula
Abstract: I describe a project to formalize Euler's polyhedron formula (in the three-dimensional genus 0 form "V-E+F=2") in the MIZAR proof-checking system. I discuss in detail the particular proof of Euler's formula that is being formalized, the progress that has been made so far, what obstacles have been encountered, and what remains to be done. I will also get in to the underlying motivations for such a project, which are to evaluate the role of computer-checked formal proofs in contemporary mathematical practice and to find a place for them in the philosophy of mathematics.

Tuesday, May 15, 13:00-15:00, MPI:
Fritz Hamm, Stuttgart A computational semantics for nominalizations
Abstract: The talk introduces an event calculus originally developed by M. Shanahan for high level control of mobile robots. It is argued that a combination of the event calculus with one of Feferman's type free systems allows for a formalization of the notion reification. The combined system will be used to develop an empirically adequate computational semantic theory of nominalisations. If time allows relationships of the proposed theory to Discourse Representation Theory will be discussed.

Tuesday, May 22, 13:00-15:00, MPI:
Henk Barendregt, Nijmegen, Reflection in and on proof-assistants
Abstract: The technical notion of reflection, first employed explicitly by Gödel, denotes doing mathematics via metamathematics. It is quite useful, even indispensable, in formal mathematics. Nevertheless the goal of having a proof-assistant that makes formalizing an informal proof as easy as writing the informal argument in latex is still not reached. A view is given on the difficulties encountered. Some proposals are made for an interactive proof language.