QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge

DOI10.6092/issn.1972-5787/4570zbMath1451.68343OpenAlexW2272472459MaRDI QIDQ5195275

Florian Rabe, Michael Kohlhase

Publication date: 18 September 2019

Full work available at URL: https://doaj.org/article/4b0ad1d395b64e56960ccd75684aa736

zbMATH Keywords

QEDmathematical knowledge managementlibrary integration

Mathematics Subject Classification ID

Mathematical knowledge management (68V30)

Related Items

Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge ⋮ Making PVS accessible to generic services by interpretation in a universal format ⋮ Unnamed Item ⋮ Experiences from exporting major proof assistant libraries

Uses Software

• Coq
• Theorema
• Isabelle/HOL
• PVS
• MathWebSearch
• TPTP
• Mizar
• ProofPower
• Isabelle/jEdit
• HOL Light
• MMT
• OMDoc
• OEIS
• IMPS
• Agda
• seL4
• GitLab
• Archive Formal Proofs