Mathematical Knowledge Management

DOI10.1007/11618027MaRDI QIDQ5898516zbMATH OpenOpenAlexFDO

Authors Serge Autexier, Christoph Benzmüller, Dominik Dietrich, Andreas Meier, Claus-Peter Wirth

Publication date 12 February 2007

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

Full work available at URL https://doi.org/10.1007/11618027

Mathematics Subject Classification ID

Data structures (68P05) Knowledge representation (68T30)

Recommendations

• A proof-centric approach to mathematical assistants
• scientific article; zbMATH DE number 1629953
• Proof assistants: history, ideas and future
• Mathematical Knowledge Management
• scientific article; zbMATH DE number 2154392

Cited in

(5)

• \textsc{Plat}{\(\Omega\)}: a mediator between text-editors and proof assistance systems
• Formal Proof: Reconciling Correctness and Understanding
• \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps
• Herbrand's fundamental theorem in the eyes of Jean van Heijenoort
• Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors

Describes a project that uses

Uses Software

• OMEGA
• InKa
• Nuprl
• TPS
• Isabelle
• Coq

This page was built for publication: Mathematical Knowledge Management

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