Title: Automated HOL Light Theorem Annotation
Speaker: Timmy Gill
Abstract:

This talk will introduce my work looking to find ways to tag theorems in HOL Light corpora with their associated areas of mathematics. It is hoped that this will enhance users’ ability to understand theorems, quickly find groups of related theorems and more easily navigate libraries to find relevant lemmas for proofs. I will introduce some of the methods I propose to use to generate/ propagate tags and
describe the intuition for using them in this context.