Experiences from exporting major proof assistant libraries

DOI10.1007/s10817-021-09604-0OpenAlexW3190866889MaRDI QIDQ2069875

Florian Rabe, Michael Kohlhase

Publication date: 21 January 2022

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

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

zbMATH Keywords

exportMizarCoqIsabellePVSHOL lightIMPStheorem prover library

Mathematics Subject Classification ID

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

Related Items

A new export of the Mizar mathematical library ⋮ Extracting theory graphs from Aldor libraries

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• A scalable module system
• IMPS: An interactive mathematical proof system
• Isabelle. A generic theorem prover
• Isabelle/HOL. A proof assistant for higher-order logic
• Aligning concepts across proof assistant libraries
• Hammer for Coq: automation for dependent type theory
• Making PVS accessible to generic services by interpretation in a universal format
• Translating the IMPS theory library to MMT/OMDoc
• Theories as types
• The Mizar Mathematical Library in OMDoc: translation and applications
• HOL(y)Hammer: online ATP service for HOL Light
• Representing structural language features in formal meta-languages
• Relational data across mathematical libraries
• The Coq library as a theory graph
• A plugin to export Coq libraries to XML
• Semantics of Mizar as an Isabelle object logic
• Capturing Hiproofs in HOL Light
• The MMT API: A Generic MKM System
• Querying Proofs
• Packaging Mathematical Structures
• The Lean Theorem Prover (System Description)
• Crafting a Proof Assistant
• A framework for defining logics
• QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge
• Project Abstract: Logic Atlas and Integrator (LATIN)
• A Verified Theorem Prover Backend Supported by a Monotonic Library
• Scalable LCF-Style Proof Translation
• A Machine-Checked Proof of the Odd Order Theorem
• An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf
• Towards Knowledge Management for HOL Light
• Importing HOL Light into Coq
• A Mechanized Translation from Higher-Order Logic to Set Theory
• Types for Proofs and Programs