## 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 |