Automated Deduction and Algebra

As automated deduction software has become more widely available to the working mathematician, it has also become more useful. In this course, we will examine how to use automated deduction effectively in different areas of algebra. The particular tools we will use are Prover9, a theorem prover, and Mace4, a finite model builder, both developed by McCune. This is intended to be a practical course for mathematicians working in algebra. The goal is to become a capable user, and so we will not delve into the technical computer science side of the subject. In particular, students are not expected to have any background in the jargon of automated deduction. We will look at examples from many areas of algebra, including lattice theory, quasigroups and loops (the speaker's own area of expertise), semigroup theory and others. In Lecture I, we will discuss the basics. We will start with a general discussion of how Prover9 and software like it works, particularly the various available inference rules and the given clause algorithm. On the practical side, we will learn how to prepare input files (particularly for the Prover9-Mace4 GUI). We will run several examples (and use Mace4 to find counterexamples), and then spend time discussing basic changeable options, such as term ordering, maximum clause weights, etc. We will then look in some detail at how to interpret a Prover9 proof. This latter task is important if we take the point of view that we should learn something from a proof, not merely have a yes/no decision about the correctness of a conjecture. Students with laptops may, if they wish, bring them to the lecture and try out the software as we go. In the break between Lectures I and II, students are encouraged to download the software and try it for themselves. (And in fact, students are encouraged to do this in advance of the course: http://www.cs.unm.edu/~mccune/prover9/.) Students should also try to formulate their own problems in their areas of interest which they would like to try to attack with Prover9, and bring those problems to the lectures. In Lectures II and III, we will discuss more advanced techniques. We will look in some detail at the method of proof sketches, which uses successful proofs as "hints" for harder problems. We will look at semantic guidance, which uses finite models to force Prover9 to focus on key clauses. We will also discuss other methods of trimming the search space and how to modify effectively the given clause selection scheme. Finally, we will also look at methods for simplifying proofs. If there is time at the end, we will briefly discuss other available software such as Waldmeister and E.