Speaker: Michael Kinyon (University of Denver)
Dates/time:
20/06/2024 (Thursday), at 14:00 (UTC+1)
21/06/2024 (Friday), at 14:00 (UTC+1)
Location: Room 1.5, building VII
Title: Automated Theorem Proving and Algebra
Abstract:
This mini-course will introduce the audience to automated theorem proving (ATP) using Prover9. While ATP can, in principle, be used in any area of mathematics which has questions with first-order formulations, it has been particularly successful in various branches of algebra, such as quasigroup theory, lattice theory, semigroup theory, etc.
On the first day, I will discuss the basics of ATP systems and how they work, of setting up Prover9 input files, and some of the various settings. On the second day, I will discuss more advanced techniques, such as semantic guidance and proof sketches. One of the morals of the story I hope to tell is that an ATP system is not just a black box, but a tool you can use effectively to help you in your own research.