Classification of alignments between concepts of formal mathematical systems

DOI10.1007/978-3-319-62075-6_7zbMath1367.68309OpenAlexW2725162198WikidataQ57389271 ScholiaQ57389271MaRDI QIDQ2364703

Dennis Müller, Cezary Kaliszyk, Thibault Gauthier, Florian Rabe, Michael Kohlhase

Publication date: 21 July 2017

Full work available at URL: https://zenodo.org/record/1475071

Mathematics Subject Classification ID

Related Items (5)

Classification of alignments between concepts of formal mathematical systems ⋮ JEFL: joint embedding of formal proof libraries ⋮ Aligning concepts across proof assistant libraries ⋮ Combining higher-order logic with set theory formalizations ⋮ Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• PVS
• Why3
• Mizar
• HOL Light
• Nuprl
• MMT
• QMT
• HOLyHammer
• LATIN
• kepler98
• Whelp
• OpenTheory

Cites Work

• Unnamed Item
• A scalable module system
• HOL(y)Hammer: online ATP service for HOL Light
• Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7--11, 2014. Proceedings
• Classification of alignments between concepts of formal mathematical systems
• The MMT API: A Generic MKM System
• Sharing HOL4 and HOL Light Proof Knowledge
• The Isabelle Framework
• Crafting a Proof Assistant
• Project Abstract: Logic Atlas and Integrator (LATIN)
• Scalable LCF-Style Proof Translation
• Matching Concepts across HOL Libraries
• Towards Knowledge Management for HOL Light
• NNexus Reloaded
• Importing HOL Light into Coq
• A Mechanized Translation from Higher-Order Logic to Set Theory
• Types for Proofs and Programs

This page was built for publication: Classification of alignments between concepts of formal mathematical systems