Publikation
Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors
Dominik Dietrich; Ewaryst Schulz; Marc Wagner
In: Intelligent Computer Mathematics - 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 208, Proceedings. Conferences on Intelligent Computer Mathematics (CICM-08), July 31 - August 1, Birmingham, United Kingdom, Pages 398-414, Lecture Notes in Artificial Intelligence (LNAI), Vol. 5144, Springer, Berlin, Heidelberg, 2008.
Zusammenfassung
Aiming at a document-centric approach to formalizing and verifying mathematics and software we integrated the proof assistance system Omega with the standard scientific text-editor Texmacs. The author writes her mathematical document entirely inside the text-editor in a controlled language with formulas in style. The notation specified in such a document is used for both parsing and rendering formulas in the document. To make this approach effectively usable as a real-time application we present an efficient hybrid parsing technique that is able to deal with the scalability problem resulting from modifying or extending notation dynamically. Furthermore, we present incremental methods to quickly verify constructed or modified proof steps by Omega. If the system detects incomplete or underspecified proof steps, it tries to automatically repair them. For collaborative authoring we propose to manage partially or fully verified documents together with its justifications and notational information centrally in a mathematics repository using an extension of OMDoc.