Formal mathematics seminar

Dozenten

• Prof. Dr. Peter Koepke

Zeit und Ort

Every second Friday, 10:15-12:00 in seminar room B, Beringstraße 4

9 Mai Bernhard Schröder "Discourse Representation Theory and its application to mathematical texts"

Discourse Representation Theory (DRT) has been devised to model dynamic aspects of natural language interpretation. As dynamic we consider those aspects of interpretation which rely on a prior textual context. Typical expressions which require a dynamic interpretation are pronouns like "she" and definite noun phrases like "the woman", called anaphorical expressions. These expressions refer to entities introduced in the prior discourse context, e.g. by existential expressions like "a woman". In mathematical texts, the function of anaphorical expressions is often taken by variables.
Furthermore, DRT models the special behavior of existential expressions in conditional contexts.
(1) If a farmer owns a donkey, he feeds it.
contains existential expressions, "a farmer" and "a donkey", but talks about farmers and donkeys in general. An analogous behaviour can be found in mathematical assumptions.
(2) Let g be a group.
starts a text section talking about groups in general.

Although standard DRT already covers a wide range of phenomena to be found in mathematical texts, variables, formulae, and the extensive use of conditions with a wide scope pose specific problems which can be addressed with slight extensions of standard DRT.

6 Juni Michael Kohlhase (Bremen) "Open Mathematical Documents, zwischen Knowledge Management und Mathematischer Praxis"

Mathematical Knowledge Management (MKM) ist eine relativ neue Forschungsrichtung im Schnittfeld zischen Mathematik und Informatik. MKM entwickelt Methoden den enormen Wissensschatz zu heben, der in konventionellen, präsentationsorientierten Medien (Artikel, Bücher, etc.) verborgen ist und mathematisches Wissen so (inhaltsorientiert) zu organisieren, däs es maschinenunterstützt zugänglich gemacht werden kann. Auf der anderen Seite scheint - ihrer Natur nach - die Mathematik eine besonders gegeignete Disziplin um innovative Konzepte für inhaltsbasierte Systeme, semantische Interoperabilität, und das Semantic Web zu erproben.

Wir haben in der letzten Dekade das OMDoc Format als einen Beitrag zum MKM entwickelt. Es handelt sich dabei um ein offenes XML-basietes Format, das mathematisches Wissen auf der Dokumenten-, Objekt-, Aussagen- und der Theorieebene repräsentieren kann. Ich werde das OMDoc Format und die zugrundeliegenden Annahmen über die Struktur mathematischen Wissens vorstellen

Auf dieser Basis möchte ich OMDoc-kompatible Software-Systeme und geplante Arbeiten zur Semantik-Extraktion aus grossen mathematisch/technischen Korpora wie den Cornell ePrint Archive (http://www.arxiv.org) vorstellen. Weiterhin möchte ich diskutieren, welche Spracherweiterungen notwendig sind, um OMDoc auf andere Wissenschaften zu erweitern (Mathematik ist die Sprache der Wissenschaft).

13 Juni Christoph Benzmueller (Saarbruecken) Tool Support for Formalized Mathematics: Cooperative Higher-Order Theorem Proving with LEO-II, Tutorial Dialogues on Proofs with the DIALOG demonstrator, and the PLATO/OMEGA Proof Assistant Plug-in for TeXmacs

LEO-II is a standalone, resolution-based higher-order ATP that is designed for fruitful cooperation with specialist provers for fragments of higher-order logic. The idea is to combine the strengths of the different systems. On the other hand, LEO-II itself, as an external reasoner, is designed to support \higher-order proof assistants such as Isabelle/HOL, HOL, and \OMEGA by efficiently automating subproblems and thereby reducing user effort. We show that the cooperative theorem proving approach outperforms -- modulo different problem representations -- first-order ATPs such as Vampire on problems about sets, relations, and functions.

In the DIALOG project we have revealed and addressed foundational research challenges that are crucial for realizing intelligent computer-supported proof tutoring based on a flexible, natural language-based dialogue between student and computer. In the proof tutoring scenario as studied in the project the student communicates proof steps to the tutorial system by embedding them in natural language utterances. The language used is a mixture of natural-language and mathematical expressions. Proof construction is performed in a stepwise fashion, and the demonstrator system responds to utterances with appropriate didactically useful feedback or also with hints.

The PLATO tool integrates the proof assistant system OMEGA with the scientific texteditor TeXmacs. The general idea is to integrate semantic-based services for mathematics into the scientific wysiwyg text-editors. The user may help the system to understand the semantics of the document by providing semantic annotations. The semantic-based services may then validate, modify or generate parts of the document. The aim is to provide useful authoring services that are invisibly running in the background without restricting the user in the way he writes his document.

2 - 5 July Sprache und Mathematik: Kann man Textbedeutungen ausrechnen? Exhibit at Wissenschaftsnacht 2008, Münsterplatz, Bonn

11 July Gregor Büchel (Köln) "A survey of software engineering with an aspect on database design"

Software Engineering ist ein Teil der Informatik, der Konzepte, Methoden und Werkzeuge für die Entwicklung komplexer Softwaresysteme (SWS) bereitstellt. Ziele und Verfahren des Software Engineering werden anhand eines Phasenmodells der Softwareentwicklung dargestellt.
Insbesondere werden Konzepte und Methoden der Spezifikation von SWS behandelt: Methoden der strukturierten Analyse, der objektorientierten Analyse (UML) und der Datenmodellierung mit Entity-Relationship-Diagrammen.
Im Zentrum des Entwurfs von SWS stehen Design-Entscheidungen. In Hinblick auf die Datenspeicherung sind unterschiedliche Arten von Persistenzmechanismen und die mit ihnen verbundene Annotation semantischer Informationen zu diskutieren (abstrakte Datentypen, Filesysteme mit Metadaten (z.B. XML-Dateisysteme), Schema-Kataloge von Datenbanken). Datenbankmanagementsysteme (DBMS) bieten unterschiedliche Möglichkeiten der Datenmodellierung und der Ausdrucksfähigkeit ihrer Anfragesprachen. Zu diesem Zweck werden Unterschiede gegebener DBMS diskutiert (relationale, objektorientierte und objektrelationale DBMS sowie native XML-DBMS).