What’s in a Theorem Name?
David Aspinall and Cezary KaliszykProceedings of the 7th Interactive Theorem Proving (ITP 2016), Lecture Notes in Computer Science 9807, pp. 459 – 465, 2016.
Abstract
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.
BibTeX
@inproceedings{DBLP:conf/itp/0001K16, 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}, }