Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors

DOI10.1007/978-3-540-85110-3_34MaRDI QIDQ5505520zbMATH OpenOpenAlexFDO

Authors Dominik Dietrich, Ewaryst Schulz, Marc Wagner

Publication date 27 January 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-85110-3_34

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Computing methodologies for text processing; mathematical typography (68U15)

Recommendations

• Mathematical Knowledge Management
• scientific article; zbMATH DE number 2079832
• Supporting the formal verification of mathematical texts
• Towards a formally verified proof assistant
• scientific article; zbMATH DE number 1696759
• A Framework for Interactive Proof
• scientific article; zbMATH DE number 500942
• Interactive and probabilistic proof-checking

Cites work

• A Formal Correspondence Between OMDoc with Alternative Proofs and the ${\overline{\lambda}\mu\tilde{\mu}}$ -Calculus
• scientific article; zbMATH DE number 1693497 (Why is no real title available?)
• scientific article; zbMATH DE number 1980938 (Why is no real title available?)
• Mathematical Knowledge Management
• Spurious Disambiguation Error Detection
• Supporting User-Defined Notations When Integrating Scientific Text-Editors with Proof Assistance Systems
• Synthesizing Proof Planning Methods and Ω-Ants Agents from Mathematical Knowledge
• The Layers of Logiweb

Cited in

(8)

• Proof assistants: history, ideas and future
• Towards semantic mathematical editing
• scientific article; zbMATH DE number 1696759 (Why is no real title available?)
• \textsc{Plat}{\(\Omega\)}: a mediator between text-editors and proof assistance systems
• Managing proof documents for asynchronous processing
• Large formal wikis: issues and solutions
• Supporting User-Defined Notations When Integrating Scientific Text-Editors with Proof Assistance Systems
• Mathematical Knowledge Management

Describes a project that uses

Uses Software

• TeXmacs
• Mizar
• Isar
• MAYA

This page was built for publication: Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors

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