You're currently viewing an old version of this dataset. To see the current version, click here.

HOL Light and Flyspeck corpora

The dataset consists of the core HOL Light corpus and the Flyspeck corpus, with millions of nodes representing atomic inferences.

Data and Resources

This dataset has no data

Cite this as

Cezary Kaliszyk, Josef Urban (2024). Dataset: HOL Light and Flyspeck corpora. https://doi.org/10.57702/k3dte6ep

Private DOI This DOI is not yet resolvable.
It is available for use in manuscripts, and will be published when the Dataset is made public.

Additional Info

Field Value
Created December 3, 2024
Last update December 3, 2024
Defined In https://doi.org/10.48550/arXiv.1310.2797
Author Cezary Kaliszyk
More Authors
Josef Urban
Homepage http://mizar.cs.ualberta.ca/~mptp/lemma_mining/