Supporting User-Defined Notations When Integrating Scientific Text-Editors with Proof Assistance Systems

DOI10.1007/978-3-540-73086-6_16MaRDI QIDQ5428269zbMATH OpenOpenAlexFDO

Authors Serge Autexier, Armin Fiedler, Thomas Neumann, Marc Wagner

Publication date 28 November 2007

Published in Towards Mechanized Mathematical Assistants (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73086-6_16

Mathematics Subject Classification ID

Computing methodologies for text processing; mathematical typography (68U15)

Recommendations

• Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors
• \textsc{Plat}{\(\Omega\)}: a mediator between text-editors and proof assistance systems
• Mathematical Knowledge Management
• scientific article; zbMATH DE number 1696759
• MMTTeX: connecting content and narration-oriented document formats

Cited in

(4)

• \textsc{Plat}{\(\Omega\)}: a mediator between text-editors and proof assistance systems
• Formal Proof: Reconciling Correctness and Understanding
• Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors
• From Notation to Semantics: There and Back Again

Describes a project that uses

Uses Software

• Isabelle/HOL
• TeXmacs
• Matita
• OMDoc
• Plat-Omega
• MATHsAiD
• LaTeX

This page was built for publication: Supporting User-Defined Notations When Integrating Scientific Text-Editors with Proof Assistance Systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5428269)