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.
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 language | English |
|---|---|
| Title of host publication | Proceedings of ITP 2016: Interactive Theorem Proving 7th International Conference |
| Publisher | Springer, Cham |
| Pages | 459-465 |
| Number of pages | 7 |
| ISBN (Electronic) | 978-3-319-43144-4 |
| ISBN (Print) | 978-3-319-43143-7 |
| DOIs | |
| Publication status | Published - 7 Aug 2016 |
| Event | Interactive Theorem Proving 7th International Conference - Nancy, France Duration: 22 Aug 2016 → 27 Aug 2016 https://itp2016.inria.fr/ |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer, Cham |
| Volume | 9807 |
| ISSN (Print) | 0302-9743 |
Conference
| Conference | Interactive Theorem Proving 7th International Conference |
|---|---|
| Abbreviated title | ITP 2016 |
| Country/Territory | France |
| City | Nancy |
| Period | 22/08/16 → 27/08/16 |
| Internet address |