What’s in a Theorem Name?

David Aspinall, Cezary Kaliszyk

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

ITPs use names for proved theorems. Good names are either widely known or descriptive, corresponding to a theorem’s statement. Good names should be consistent with conventions, and be easy to remember. But thinking of names like this for every intermediate result is a burden: some developers avoid this by using consecutive integers or random hashes instead. We ask: is it possible to relieve the naming burden and automatically suggest sensible theorem names? We present
a method to do this. It works by learning associations between existing theorem names in a large library and the names of defined objects and term patterns occurring in their corresponding statements.
Original languageEnglish
Title of host publicationProceedings of ITP 2016: Interactive Theorem Proving 7th International Conference
PublisherSpringer, Cham
Number of pages7
ISBN (Electronic)978-3-319-43144-4
ISBN (Print)978-3-319-43143-7
Publication statusPublished - 7 Aug 2016
EventInteractive Theorem Proving 7th International Conference - Nancy, France
Duration: 22 Aug 201627 Aug 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer, Cham
ISSN (Print)0302-9743


ConferenceInteractive Theorem Proving 7th International Conference
Abbreviated titleITP 2016
Internet address

Cite this