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

DOI10.1007/978-3-540-85110-3_34zbMath1166.68342OpenAlexW1488706998MaRDI QIDQ5505520

Ewaryst Schulz, Dominik Dietrich, Marc Oliver 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)

Related Items

Managing Proof Documents for Asynchronous Processing ⋮ Proof assistants: history, ideas and future

Uses Software

• MAYA
• Isar
• Mizar
• TeXmacs

Cites Work

• Unnamed Item
• Unnamed Item
• Supporting User-Defined Notations When Integrating Scientific Text-Editors with Proof Assistance Systems
• The Layers of Logiweb
• Spurious Disambiguation Error Detection
• A Formal Correspondence Between OMDoc with Alternative Proofs and the ${\overline{\lambda}\mu\tilde{\mu}}$ -Calculus
• Synthesizing Proof Planning Methods and Ω-Ants Agents from Mathematical Knowledge
• Mathematical Knowledge Management