Abstract

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.

BibTeX

@Article{tgck-jsc18,
  author =       {Thibault Gauthier and Cezary Kaliszyk},
  title =        {Aligning Concepts across Proof Assistant Libraries},
  journal =      {J. Symbolic Computation},
  volume    = {90},
  pages     = {89--123},
  year      = {2019},
  url       = {https://doi.org/10.1016/j.jsc.2018.04.005},
  doi       = {10.1016/j.jsc.2018.04.005},
}