Naproche - Natural Language Proof Checking
"; ?>

Seminar Formale Mathematik

Dozenten

Zeit und Ort

Freitags 10-12 im Zimmer 006.

Inhalt

Vorträge von internen und externen Referenten über Formale Mathematik, d.h., über die axiomatische Durchführung von Mathematik in strikt formalen Sprachen mit strikt formalen Ableitungsregeln. Im Zusammenhang mit dem lokalen Projekt NaProChe (Natural language Proof Checking) wird besonders die Frage diskutiert, inwieweit durch den Einsatz von Softwaresystemen strikt formale Systeme aufgebaut werden können, die für den Benutzer "natürlich" im Sinne des gewöhnlichen mathematischen Arbeitens sind. Das bezieht sich auf Benutzerschnittstellen, verwendete Sprache, Theorien und Beweismethoden.

Die Vorträge finden etwa 14-tägig statt. 


Friday, June 18, 10:15-12:00, EA 60, Room N0.007 (Nebengebäude)
John Mumma, Euclid’s diagrams and the primitive concepts of elementary geometry
Abstract: One thing a formalization of a mathematical theory provides is a sharp classification of the theory’s concepts as either primitive or defined. In this talk, I examine how this separation is made in two formalizations of Euclid’s elementary plane geometry: the axiomatization presented in Tarski’s `What is elementary geometry?’, and the formal system E. The latter is a system that has recently been developed to illuminate the role of diagrams in the proofs in the Elements. In accounting for Euclid’s diagrams, E classifies more geometric relations as primitive than Tarski’s formalization does. At the same time, the logic of E is much weaker. I show what this trade-off amounts to precisely by describing E as a formal system and sketching the proof that E is complete relative to Tarksi’s theory.

Former Terms


 

Last changed June 6st 2010