PlatΩ: a mediator between text-editors and proof assistance systems. We present a generic mediator, called PlatΩ, between text-editors and proof assistants. PlatΩ 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 PlatΩ automatically generates the corresponding formal representation for a proof assistant, in our case Ωmega. The primary task of PlatΩ is the maintenance of consistent formal and informal representations during the interactive development of the document.
Keywords for this software
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Rabe, Florian: MMTTeX: connecting content and narration-oriented document formats (2019)
- Autexier, Serge; Fiedler, Armin; Neumann, Thomas; Wagner, Marc: Supporting user-defined notations when integrating scientific text-editors with proof assistance systems (2007)
- Wagner, Marc; Autexier, Serge; Benzmüller, Christoph: \textscPlat(\Omega): a mediator between text-editors and proof assistance systems (2007)