PlatΩ: A Mediator between Text-Editors and Proof Assistance Systems

DOI10.1016/J.ENTCS.2006.09.024zbMath1278.68284OpenAlexW2108920859MaRDI QIDQ2867939

Serge Autexier, Christoph Benzmüller, Marc Oliver 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

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

Mathematics Subject Classification ID

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

Related Items (3)

Tactics for hierarchical proof ⋮ Managing Proof Documents for Asynchronous Processing ⋮ Isabelle as Document-Oriented Proof Assistant

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Grammatical Framework
• Automated Deduction – CADE-20
• Types for Proofs and Programs
• Mechanizing Mathematical Reasoning
• Synthesizing Proof Planning Methods and Ω-Ants Agents from Mathematical Knowledge
• Mathematical Knowledge Management
• Mathematical Knowledge Management
• Mathematical Knowledge Management
• Mathematical Knowledge Management

This page was built for publication: PlatΩ: A Mediator between Text-Editors and Proof Assistance Systems