What’s in a Theorem Name?

David Aspinall and Cezary Kaliszyk

Proceedings of the 7th Interactive Theorem Proving (ITP 2016), Lecture Notes in Computer Science 9807, pp. 459 – 465, 2016.


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.


  PDF |    doi:10.1007/978-3-319-43144-4_28  |  © Springer International Publishing Switzerland


author = {David Aspinall and Cezary Kaliszyk},
title = {What's in a Theorem Name?},
booktitle = {Interactive Theorem Proving - 7th International Conference, {ITP}
2016, Nancy, France, August 22-25, 2016, Proceedings},
pages = {459--465},
year = {2016},
editor = {Jasmin Christian Blanchette and Stephan Merz},
series = {Lecture Notes in Computer Science},
volume = {9807},
publisher = {Springer},
Nach oben scrollen