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, April 15, 11:15-13:00 (one hour later than usual!), EA 60, Room 1.007
Marco Caminati, Classical model theory in Mizar
Abstract: I have formalized Lindenbaum lemma, satisfiability, Godel's completeness and Lowenheim-Skolem theorems in Mizar, using a simplified, unified and coherent framework to encode model theory.
I will describe this framework, focusing in particular on the simplified syntax for first-order languages (only two special symbols, and no need for constant symbols) and on the sequent derivation rules adopted (not requiring to define the concept of free occurrence).
Then I will show how those constructions were used for a new, Henkin-like, scheme to prove the results hinted above, with emphasis on the role of each single derivation rule, and on when some standard definitions (consistency, maximality, rule correctness) of model theory actually need to come into play.
If time permits, I will also discuss some aspects of the Mizar implementation of the aforementioned syntax and sequent calculus."

Former Terms


 

Last changed June 6st 2010