\textsc{Plat}{}: a mediator between text-editors and proof assistance systems

DOI10.1016/J.ENTCS.2006.09.024MaRDI QIDQ2867939zbMATH OpenOpenAlexFDO

Authors Serge Autexier, Christoph Benzmüller, Marc Wagner

Publication date 20 December 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2006.09.024

zbMATH Keywords

proof-assistance systemsTexmacstext-editoruser interface{\(\Omega\)}\textsc{mega}

Mathematics Subject Classification ID

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

Recommendations

• Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors
• Supporting User-Defined Notations When Integrating Scientific Text-Editors with Proof Assistance Systems
• \(\Omega\)\textsc{mega}: towards a mathematical assistant
• Mathematical Knowledge Management
• scientific article; zbMATH DE number 1696759

Cites work

• Automated Deduction – CADE-20
• Grammatical Framework
• scientific article; zbMATH DE number 1980938 (Why is no real title available?)
• scientific article; zbMATH DE number 2079831 (Why is no real title available?)
• scientific article; zbMATH DE number 1765686 (Why is no real title available?)
• scientific article; zbMATH DE number 3331288 (Why is no real title available?)
• Mathematical Knowledge Management
• Mathematical Knowledge Management
• Mathematical Knowledge Management
• Mathematical Knowledge Management
• Mechanizing Mathematical Reasoning
• Synthesizing Proof Planning Methods and Ω-Ants Agents from Mathematical Knowledge
• Types for Proofs and Programs

Cited in

(4)

• Managing proof documents for asynchronous processing
• Isabelle as document-oriented proof assistant
• Supporting User-Defined Notations When Integrating Scientific Text-Editors with Proof Assistance Systems
• Tactics for hierarchical proof

Describes a project that uses

Uses Software

• Isar
• Automath
• OMDoc
• MAYA
• Theorema
• Pcoq
• GF
• Omega-ANTS
• OMEGA
• Plat-Omega
• LOUI
• XPath
• Multi

This page was built for publication: \textsc{Plat}{\(\Omega\)}: a mediator between text-editors and proof assistance systems

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