Mathematical Knowledge Management

DOI10.1007/11618027zbMATH Open1151.68628OpenAlexW2480281325MaRDI QIDQ5898516FDOQ5898516

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

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

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

Mathematics Subject Classification ID

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

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

Uses Software

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

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)