Seminar Formale Mathematik
Dozenten
- Prof. Dr. Peter Koepke
- Prof. Dr. Bernhard Schröder
Zeit und Ort
Freitags 10-12 im Seminarraum B, Beringstraße 4
Inhalt
Friday, October 31, 10:00-12:00, Beringstr. 4 Seminarraum B
Serge Autexier, Stephan Busemann, Marc Wagner, Semantik-basierte Autorenwerkzeuge für mathematische Dokumente
Abstract:
Die Erstellung von Dokumenten mit mathematischen Inhalten stellt
höchste Ansprüche an die typographische Qualität, denen in
existierenden Autorenwerkzeugen Rechnung getragen wird, etwa in
TeX-basierten Systemen und neuerdings auch in Word 2007. Dahingegen
bieten diese nur mangelhafte Unterstützung für die Überprüfung der
Inhalte -- etwa die konsistente Verwendung von Notationen oder
Zyklenfreiheit und ggf. Verifikation definitorischer und
argumentativer Strukturen -- sowie für darauf aufbauende erweiterte
Editier-Operationen, wie die Eingliederung von Teildokumenten in ein
Gesamtdokument oder die Umgestaltung eines Dokuments. Ziel des
VerimathDoc-Projektes ist die Entwicklung von Methoden und Techniken,
um semantik-basierte Assistenzwerkzeuge in existierende
Autorenwerkzeuge zu integrieren. Grundprinzip hierbei ist der Einsatz
computerlinguistischer Textanalyse-Verfahren, um den Inhalt eines
Dokuments in semi-formale und schließlich auch formallogische
Strukturen zu überführen, auf deren Grundlage entsprechende
Unterstützung bereitgestellt werden kann, wie sie zum Teil bereits in
interaktiven Beweisassistenzsystemen existiert. Daraus resultierende
Modifikationen und Erweiterungen der Strukturen sollen anschließend
mit Hilfe von Textgenerierungs-Verfahren wieder in das Dokument
integriert werden können.
Dieser Vortrag gibt einen Überblick über die allgemeinen Ziele und den
aktuellen Stand des VerimathDoc-Systems, welches derzeit das
Beweisassistenzsystem OMEGA mit Hilfe des Mediators Plato transparent
mit dem Texteditor TeXmacs verbindet. Weiterhin gibt er einen
Überblick, wie die verschiedenen Themenkomplexe aus den Gebieten der
Computerlinguistik, Informatik, und interaktiven
Beweisassistenzsysteme im Speziellen behandelt wurden bzw. künftig
behandelt werden sollen.
Friday, November 21, 10:00-12:00, Beringstr. 4 Seminarraum B
Norbert Fuchs, Attempto