Classification of alignments between concepts of formal mathematical systems

DOI10.1007/978-3-319-62075-6_7MaRDI QIDQ2364703zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Dennis Müller, T. Gauthier, Cezary Kaliszyk, Michael Kohlhase, Florian Rabe

Publication date 21 July 2017

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

Mathematics Subject Classification ID

Knowledge representation (68T30) Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35)

Recommendations

• scientific article; zbMATH DE number 4016680
• Formal systems of constructive mathematics
• GALOIS CONNECTIONS AND FORMAL CONCEPT ANALYSIS
• scientific article; zbMATH DE number 877297
• scientific article; zbMATH DE number 1522654
• Toward an algebraic theory of systems
• scientific article; zbMATH DE number 1318482
• A classification of mathematical concepts
• scientific article; zbMATH DE number 4070873
• Features of interaction between formal concept analysis and algebraic geometry

Cites work

• A mechanized translation from higher-order logic to set theory
• A scalable module system
• Classification of alignments between concepts of formal mathematical systems
• Crafting a Proof Assistant
• HOL(y)Hammer: online ATP service for HOL Light
• scientific article; zbMATH DE number 1863394 (Why is no real title available?)
• Importing HOL Light into Coq
• Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7--11, 2014. Proceedings
• Matching concepts across HOL libraries
• NNexus reloaded
• Project abstract: logic atlas and integrator (LATIN)
• Scalable LCF-style proof translation
• Sharing HOL4 and HOL Light proof knowledge
• The Isabelle Framework
• The MMT API: a generic MKM system
• Towards Knowledge Management for HOL Light
• Types for Proofs and Programs

Cited in

(7)

• Aligning concepts across proof assistant libraries
• Classification of alignments between concepts of formal mathematical systems
• Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
• Combining higher-order logic with set theory formalizations
• Indexing and retrieval in a heterogeneous formal library
• Supporting maintenance of formal mathematics with similarity search
• JEFL: joint embedding of formal proof libraries

Describes a project that uses

Uses Software

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

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

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