Department of Mathematics
Server

Sir Roger Penrose once remarked that computers are intrinsically limited, compared to humans, when it comes to the doing of mathematics. Even those who think that such things can be proved may be interested in the empirical question: what kind of mathematics can computers do? Can a computer reason logically like humans and prove new theorems? A partial answer can be given using modern automated reasoning software such as Otter and Prover9. Otter, developed by William McCune at the Argonne National Laboratory, is the first widely used high-performance theorem prover. It is based on first-order inference rules, substitution principles, unification etc (see [1], [2]). Otter has since been replaced by Prover9, which is paired with Mace4, a counter-example generator. Both are available free for Mac OSX, Windows and the Unix platforms. In this presentation, we plan to give a brief survey of this relatively new area of experimental mathematics and give a list of "new" theorems proved with the help of these two theorem-provers. In particular, we plan to show some live demonstrations of automated deduction in the following areas of algebra:

1. Ring theory - some new commutativity theorems (in collaboration with Yang Zhang)
2. Semigroups - cancellation laws and group-like deductions
3. Moufang loops - finite models - using Skolem functions
4. Counter-examples as ring models
5. Group theory - presentation of the trivial group and Andrews- Curtis conjecture
6. (gL)-algebras- Cayley-Bacharach implications of algebraic geometry
7. Lattice theory - uniquely complemented lattices and Huntington laws

References:

1. Larry Wos and Gail W. Pieper. A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning, World Scientific, 2006.
2. J. D. Phillips, See Otter digging for algebraic pearls, Quasigroups and Related Systems 10 (2003), 95-114.
3. David Kelly; R. Padmanabhan. Another independent self-dual basis for the trivial variety. Algebra Universalis 57 (2007), no. 4, 497--499.
4. R. Padmanabhan; W. McCune; R. Veroff. Lattice laws forcing distributivity under unique complementation. Houston J. Math. 33 (2007), no. 2, 391--401.
5. R. Padmanabhan; W. McCune. Uniqueness of Steiner laws on cubic curves. Beitr?ge Algebra Geom. 47 (2006), no. 2, 543--557.
6. R. Padmanabhan; W. McCune; R. Veroff. Levi's commutator theorems for cancellative semigroups. Semigroup Forum 71 (2005), no. 1, 152--157.
7. R. Padmanabhan; Peter Penner. A hyperbase for binary lattice hyperidentities. J. Automat. Reason. 24 (2000), no. 3, 365--370.
8. R. Padmanabhan; Yang Zhang. Automated Deduction in Ring Theory (to appear).