Aligning concepts across proof assistant libraries
| Autor: | Thibault Gauthier, Cezary Kaliszyk |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Algebra and Number Theory
Matching (graph theory) Programming language Process (engineering) 010102 general mathematics Proof assistant HOL 010103 numerical & computational mathematics Mizar system Intuitionistic type theory computer.software_genre 01 natural sciences Computational Mathematics TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Similarity (psychology) Set theory 0101 mathematics computer Mathematics |
| Zdroj: | Journal of Symbolic Computation |
| ISSN: | 0747-7171 |
| DOI: | 10.1016/j.jsc.2018.04.005 |
| Popis: | As the knowledge available in the computer understandable proof corpora grows, recognizing repeating patterns becomes a necessary requirement in order to organize, synthesize, share, and transmit ideas. In this work, we automatically discover patterns in the libraries of interactive theorem provers and thus provide the basis for such applications for proof assistants. This involves detecting close properties, inducing the presence of matching concepts, as well as dynamically evaluating the quality of matches from the similarity of the environment of each concept. We further propose a classification process, which involves a disambiguation mechanism to decide which concepts actually represent the same mathematical ideas. We evaluate the approach on the libraries of six proof assistants based on different logical foundations: HOL4, HOL Light, and Isabelle/HOL for higher-order logic, Coq and Matita for intuitionistic type theory, and the Mizar Mathematical Library for set theory. Comparing the structures available in these libraries our algorithm automatically discovers hundreds of isomorphic concepts and thousands of highly similar ones. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect