Automated HOL Light Theorem Annotation

Date: 16th October 2020

Time: 14:00-16:00

Location: Online


Title: Automated HOL Light Theorem Annotation
Speaker: Timmy Gill

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.