Experiences from exporting major proof assistant libraries

DOI10.1007/S10817-021-09604-0MaRDI QIDQ2069875zbMATH OpenOpenAlexFDO

Authors Michael Kohlhase, Florian Rabe

Publication date 21 January 2022

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2005.03089

zbMATH Keywords

exportCoqIsabelleMizarPVSHOL lightIMPStheorem prover library

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• scientific article; zbMATH DE number 1951627
• Toward sharing libraries of mathematics between theorem provers
• A new export of the Mizar mathematical library
• Mathematical Knowledge Management
• FoCaLiZe and Dedukti to the rescue for proof interoperability

Cites work

• scientific article; zbMATH DE number 1951640 (Why is no real title available?)
• scientific article; zbMATH DE number 1863394 (Why is no real title available?)
• A framework for defining logics
• A machine-checked proof of the odd order theorem
• A mechanized translation from higher-order logic to set theory
• A plugin to export Coq libraries to XML
• A scalable module system
• A verified theorem prover backend supported by a monotonic library
• Aligning concepts across proof assistant libraries
• An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf
• Capturing hiproofs in HOL light
• Crafting a Proof Assistant
• HOL(y)Hammer: online ATP service for HOL Light
• Hammer for Coq: automation for dependent type theory
• IMPS: An interactive mathematical proof system
• Importing HOL Light into Coq
• Isabelle. A generic theorem prover
• Isabelle/HOL. A proof assistant for higher-order logic
• Making PVS accessible to generic services by interpretation in a universal format
• Packaging Mathematical Structures
• Project abstract: logic atlas and integrator (LATIN)
• QED reloaded: towards a pluralistic formal library of mathematical knowledge
• Querying proofs
• Relational data across mathematical libraries
• Representing structural language features in formal meta-languages
• Scalable LCF-style proof translation
• Semantics of Mizar as an Isabelle object logic
• The Coq library as a theory graph
• The Lean theorem prover (system description)
• The MMT API: a generic MKM system
• The Mizar Mathematical Library in OMDoc: translation and applications
• Theories as types
• Towards Knowledge Management for HOL Light
• Translating the IMPS theory library to MMT/OMDoc
• Types for Proofs and Programs

Cited in

(3)

• A new export of the Mizar mathematical library
• Toward sharing libraries of mathematics between theorem provers
• Extracting theory graphs from Aldor libraries

Describes a project that uses

Uses Software

• Whelp
• CoqInE
• CoqHammer
• kepler98
• LATIN
• seL4
• Lean
• HOLyHammer
• IMPS
• SPARQL
• OMDoc
• QMT
• MMT
• Nuprl
• HOL Light
• ETPS
• Mizar
• PVS
• Isabelle/HOL
• Isabelle
• Coq

This page was built for publication: Experiences from exporting major proof assistant libraries

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