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 17, 10:15-12:00, EA 60, Room 006
Andrei Paskevich, ForTheL: design decisions [not [yet] taken]
Abstract: Historically, the best-known and most powerful proof assistants were the systems with quite specific logical foundations, input languages, and proof development tools. This created a considerable barrier for newcomers, even for those who were experienced in formal mathematics. In recent years, however, the idea to lower this barrier -- by using (elements of) natural language in the input, by adopting traditional "declarative" style of proof, by abstracting over the particularities of a given verifier -- gained a lot of attention, and a number of new projects have emerged.
In this talk, we present a formal language, called ForTheL, which imitates the natural language and style of "human" mathematical texts. This language is used as the input language of SAD, a proof assistant intended for automated proof verification. We demonstrate that ForTheL allows for terse and comprehensible formalizations and describe its syntax and semantics with respect to verification. We also enumerate the features that the current realization of ForTheL is lacking and discuss the ways to address these shortcomings.

Thursday, Mai 14, EA 60, Room 208 until 16:30 and then Room 107
Workshop VeriMathDoc - Naproche
9:00 - 11:00 Session Formalisierung Formalisierung: Es gibt i.A. mehrere Möglichkeiten, wie die beschriebenen Konzepte in Logik formalisiert werden (Beispiel: der Begriff einer "Klasse" als Sorte/Typ oder als Praedikat). Je nachdem wie man sich entscheidet, hat das Vor- und Nachteile und es scheint keine a priori bessere Art zu formalisieren zu geben. Aber, in dem Prozess nach der Textanalyse hin zum Beweissystem muss die Entscheidung getroffen werden und die Frage ist wie man sie trifft, welche Probleme es hier gibt und allgemein, wie kann man damit umgehen, dass es Alternativen gibt?

- Vortrag "Möglichkeiten Klassen zu formalisieren"
- Diskussion:
+ Inwieweit legen wir die Art der Formalisierung in den Systemen fest?
+ Falls wir sie nicht festlegen, wie kann der Autor sie angeben?
+ Wollen wir mit alternativen Formalisierungen umgehen koennen?
- Fazit und Planung bis zum nächsten Treffen

11:00 - 13:00: Session Corpora of Documents
Sowohl VeriMathDoc als auch Naproche benötigen Beispieltexte um die Fähigkeiten des jeweiligen Systems zu demonstrieren. In dieser Session wollten wir erörtern inwieweit eine gemeinsame Sammlung möglich ist.
- Vortrag Syntax Naproche ( 15 - 30 min)
- Vortrag Syntax VeriMathDoc ( 15 - 30 min)
- Diskussion:
+ Ist eine gemeinsame Syntax möglich? Wie müsste man die bestehenden erweitern/anpassen.
+ Welche Arten von Dokumente (vollstaendig/Fragmente) wollen wir annotieren und in welchen Formaten? Wie wollen wir darin suchen koennen? Wo bekommen wir die her?
- Fazit und Planung bis zum nächsten Treffen

13:00 - 14:00 Mittagessen

14:00 - 16:00: Session Textanalyse
Beide Projekte verwenden sehr verschiedene Methoden zur Textanalyse. Was die Probleme der jeweiligen Methoden, und was könnten Lösungsansätze sein.
- Vortrag Probleme Textanalyse Naproche ( ~15 min)
- Vortrag Probleme Textanalyse VeriMathDoc ( ~15 min)
- Diskussion: Kann man die die Methoden kombinieren um die Probleme zu lösen.
+ Wie gehen wir mit Fehlschlägen in der Textanalyse um? Wie geht man mit Texten um, die man erkennbar nur partiell analysieren kann? Sind partielle Analyseergebnisse (etwa aus einer Chart) verwendbar?
+ Domänenspezifische Semantik/Pragmatik: Können wir Meta-Aussagen (zB "Wir geben nun zwei weitere Regeln für das Rechnen mit Vektorprodukten an, von denen wir die erste gleich und die zweite im nächsten Abschnitt beweisen werden." [1]) mit flachen Verfahren hinreichend erkennen?
- Fazit und Planung bis zum nächsten Treffen

16:00 - 16:30 Kaffee

16:30 - 18:30 Session: Beweistechniken
Abgesehen von den angeschlossenen Beweisern ist oft auch eine Vorverarbeitung wünschenswert. Was wurde hier schon implementiert, welche Probleme sind aufgetreten.
- Vortrag Beweistechniken Naproche ( 15 - 30 min)
- Vortrag Beweistechniken VeriMathDoc ( 15 - 30 min)
- Diskussion:
+ Potentielle Problemlösungen
- Fazit und Planung bis zum nächsten Treffen

Friday, May 29, 10:15-12:00, EA 60, Room 006
Marcos Cramer: The Naproche Project, Controlled Natural Language Proof Checking of Mathematical Texts
Abstract: This is the talk that we will give at the CNL (Controlled Natural Language) Conference in Marettimo in June.
We will discuss the Semi-Formal Language of Mathematics, present the Naproche CNL that is based on it, and explain the Proof Representation Structures that can be derived from a Naproche text.
- Extended Abstract of this talk

Friday, June 19, 10:15-11:00, EA 60, Room 006
Daniel Kuehlwein: The Naproche System
Abstract: This is the talk that we will give at the Calculemus Conference.
We give an introduction to the Naproche System.
- Extended Abstract of this talk

Friday, June 19, 11:15-12:00, EA 60, Room 006
Sebastian Zittermann: Scheme2XML
Abstract: Der Vortrag stellt das Programm Scheme2XML vor. Scheme2XML erstellt aus einer Datei des Texmacs-Formats "SCM" anhand vorgegebener Regeln, die in der Datei "Satz.dtd" definiert sind, eine XML-Datei und überprüft diese auf Validität.
- Zugrundeliegende Bachelorarbeit

Former Terms


 

Last changed October 12st 2009