Bonn Mathematical Logic Group

Seminar Formale Mathematik

Dozenten

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

 

Last updated: 14 October 2008