Integrating Proof Assistants as Reasoning and Verication Tools into a Scientic WYSIWYG Editor
Henri Lesourd · 2005
A major problem for the acceptance of mathematical proof assistance systems in mathematical practise is the shortcomings of their user interfaces. Often the interfaces are developed bottom-up starting from the mathematical proof assistance system. Therefore they usually focus on the individual system and its proof development paradigm and neglect traditional forms to communicate proofs as used by mathematicians. To address this problem we propose a top-down approach where we start from an existing scientic WYSIWYG text editor which supports the preparation of mathematical publications in high quality typesetting and integrate a mathematical proof assistance system to support proof development and validation. Concretely, we extend the document format of the text editor by semantic markup to encode formal mathematical content and to communicate with the formal system. Additionally we provide interaction markup dening contextsensitive means to control the mathematical proof assistance system through the text editor.