What's in a theorem name?

DOI10.1007/978-3-319-43144-4_28MaRDI QIDQ2829279zbMATH OpenOpenAlexFDO

Authors Cezary Kaliszyk, D. Aspinall

Publication date 27 October 2016

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://www.pure.ed.ac.uk/ws/files/25410118/namespark_short_1.pdf

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Learning-assisted theorem proving with millions of lemmas
• Lemma Mining over HOL Light
• Proving theorems by reuse
• scientific article; zbMATH DE number 1552515
• Note on the benefit of proof representations by name

Cites work

• Four decades of \textsc{Mizar}. Foreword
• Matching concepts across HOL libraries

Cited in

(2)

• Aligning concepts across proof assistant libraries
• Deep Generation of Coq Lemma Names Using Elaborated Terms

Describes a project that uses

Uses Software

• kepler98
• HOL

This page was built for publication: What's in a theorem name?

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829279)