Matching Concepts across HOL Libraries

DOI10.1007/978-3-319-08434-3_20zbMath1304.68154arXiv1405.3906OpenAlexW86012225WikidataQ108482167 ScholiaQ108482167MaRDI QIDQ5495929

Thibault Gauthier, Cezary Kaliszyk

Publication date: 7 August 2014

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Knowledge representation (68T30)

Related Items (11)

Classification of alignments between concepts of formal mathematical systems ⋮ A survey on retrieval of mathematical knowledge ⋮ JEFL: joint embedding of formal proof libraries ⋮ Structure Formation in Large Theories ⋮ Aligning concepts across proof assistant libraries ⋮ Automating formalization by statistical and semantic parsing of mathematics ⋮ FoCaLiZe and Dedukti to the rescue for proof interoperability ⋮ Making PVS accessible to generic services by interpretation in a universal format ⋮ Unnamed Item ⋮ What’s in a Theorem Name? ⋮ Towards Knowledge Management for HOL Light

Uses Software

• Isabelle
• Isabelle/HOL
• MoMM
• HOL
• HOL Light
• MMT
• QMT
• Flyspeck
• HOLyHammer
• OpenTheory

Cites Work

• Unnamed Item
• Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings
• The HOL Light theory of Euclidean space
• HOL(y)Hammer: online ATP service for HOL Light
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Automated reasoning. Third international joint conference, IJCAR 2006, Seattle, WA, USA, August 17--20, 2006. Proceedings
• The MMT API: A Generic MKM System
• Lemma Mining over HOL Light
• HOL Light: An Overview
• A Brief Overview of HOL4
• The Isabelle Framework
• Towards Self-verification of HOL Light
• Scalable LCF-Style Proof Translation
• Data Refinement in Isabelle/HOL
• Importing HOL Light into Coq

This page was built for publication: Matching Concepts across HOL Libraries