Logik-Sem., 04.10.06, M. Wagner
Uwe Waldmann
Einladung zum Vortrag
Zeit: Mittwoch, 04.10.06, 16.15 Uhr
Ort: Hörsaal 024, MPI Saarbrücken (Geb. E1.4)
Marc Wagner (FR Informatik):
PLATO: A Mediator between Text-Editors and Proof Assistance Systems
Zusammenfassung:
We present a generic mediator, called PLATO, between text editors and
proof assistants. PLATO aims at integrated support for the development,
publication, formalization, and verification of mathematical documents
in a natural way as possible: The user authors his mathematical
documents with a scientific WYSIWYG text editor in the informal language
he is used to, that is a mixture of natural language and formulas. These
documents are then semantically annotated preserving the textual
structure by using the flexible, parameterized proof language which we
present. From this informal semantic representation PLATO automatically
generates the corresponding formal representation for a proof assistant,
in our case OMEGA. The primary task of PLATO is the maintenance of
consistent formal and informal representations during the interactive
development of the document.
______________________________________________________________________
Das Logikseminar ist eine gemeinsame Veranstaltung des DFKI, des MPI
und der Fachrichtungen Informatik, Philosophie und Rechtswissenschaft.
Vortragswünsche bitte an Uwe Waldmann, MPI, Tel.: (0681) 9325-205,
uni-intern: 92205, E-Mail: u...@mpi-sb.mpg.de