| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 6861163 | Journal of Symbolic Computation | 2019 | 35 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Artificial Intelligence
Authors
Thibault Gauthier, Cezary Kaliszyk,