Michael Kinyon (University of Denver)
Title: Automated Deduction and Algebra
Dates/times:
19/06/2023 (Monday), at 14:00–16:00
20/06/2023 (Tuesday), at 14:00–16:00
20/06/2023 (Tuesday), at 14:00–16:00
21/06/2023 (Wednesday), at 14:00–16:00
Location: Seminar room, building VII
Abstract:
This course will introduce mathematicians to the use of automated theorem provers (ATPs) such as Prover9 in algebra. The course will be taught as a mix of lecturing and hands-on practice. We will start from the basics of how to prepare input files and how to interpret proofs generated by ATPs. By the end, students will learn advanced techniques, such as proof sketches, for steering searches successfully. Examples will come from various areas of algebra where automated deduction does well, such as group theory and its generalizations (quasigroups, semigroups), lattices and order theory, and others, and occasionally from areas where automated deduction tends to be less successful, such as ring theory. Students are encouraged to bring their own research problems which they think might be amenable to ATP methods.