Matching concepts across HOL libraries
From MaRDI portal
Abstract: Many proof assistant libraries contain formalizations of the same mathematical concepts. The concepts are often introduced (defined) in different ways, but the properties that they have, and are in turn formalized, are the same. For the basic concepts, like natural numbers, matching them between libraries is often straightforward, because of mathematical naming conventions. However, for more advanced concepts, finding similar formalizations in different libraries is a non-trivial task even for an expert. In this paper we investigate automatic discovery of similar concepts across libraries of proof assistants. We propose an approach for normalizing properties of concepts in formal libraries and a number of similarity measures. We evaluate the approach on HOL based proof assistants HOL4, HOL Light and Isabelle/HOL, discovering 398 pairs of isomorphic constants and types.
Recommendations
Cites work
- A Brief Overview of HOL4
- Automated reasoning. Third international joint conference, IJCAR 2006, Seattle, WA, USA, August 17--20, 2006. Proceedings
- Data refinement in Isabelle/HOL
- HOL Light: An Overview
- HOL(y)Hammer: online ATP service for HOL Light
- Importing HOL Light into Coq
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Lemma Mining over HOL Light
- Scalable LCF-style proof translation
- Structured formal development in Isabelle
- The HOL Light theory of Euclidean space
- The Isabelle Framework
- The MMT API: a generic MKM system
- Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings
- Towards Self-verification of HOL Light
Cited in
(13)- JEFL: joint embedding of formal proof libraries
- Towards Knowledge Management for HOL Light
- Aligning concepts across proof assistant libraries
- Classification of alignments between concepts of formal mathematical systems
- scientific article; zbMATH DE number 7756106 (Why is no real title available?)
- What's in a theorem name?
- Smart matching
- Supporting maintenance of formal mathematics with similarity search
- Automatically finding theory morphisms for knowledge management
- Automating formalization by statistical and semantic parsing of mathematics
- Making PVS accessible to generic services by interpretation in a universal format
- Structure formation in large theories
- FoCaLiZe and Dedukti to the rescue for proof interoperability
Describes a project that uses
Uses Software
This page was built for publication: Matching concepts across HOL libraries
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5495929)
