What's in a theorem name?

DOI10.1007/978-3-319-43144-4_28zbMATH Open1478.68434OpenAlexW2409359688MaRDI QIDQ2829279FDOQ2829279

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

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

Mathematics Subject Classification ID

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

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

Uses Software

• HOL
• kepler98

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)