In order to foster the use of proof assistance systems, we integrated the proof assistance system OMEGA with the standard scientific text-editor TEXMACS. We aim at a document-centric approach to formalizing and verifying mathematics and software. Assisted by the proof assistance system, the author writes her document entirely inside the text-editor in a language she is used to, that is a mixture of natural language and formulas in LATEX style. The PLATO system has been designed as a support system to realize the tight integration of a proof assistance system and a text-editor. PLATO is connected with the text-editor by an annotation language which flexibly supports the usual textual structure of mathematical documents. From this informal representation PLATO automatically generates a formal representation for the proof assistance system and takes care of the propagation of changes and the service interaction. Furthermore the PLATO system provides a mechanism that allows the author to define her own notation inside a document in a natural way, which is used to parse the formulas written by the author as well as to render the formulas generated by the proof assistance system.
| [URL of the project] | plato |
| Back to Demoes of MathUI 2007 | Demoes of MathUI 2007 last updated on Sun Jun 24 2007 |