==========================================================
ADAM 2008, July 24 - 26, 2008.
University of New Mexico, Albuquerque, NM, USA.

Equational Spectra of Some Equational Classes.
(or Playing with Prover9).

by
R. Padmanabhan
University of Manitoba


In this talk, I would like to share the productive experience I had  
during the past 8 months using Prover9 and Mace4. In particular, the  
following theorems were proved directly or indirectly with the help  
of Prover9 (and with counter-examples from Mace4 to refute some of my  
conjectures).

Let K be a equational class of algebras of finite type. Following  
Alfred tarski (1968), we define mu(K) = the minimum number of  
identities needed to define K and let Nabla(K) = {n| K has an  
independent equational basis with n axioms}.

Then we have:

	1. K = the lattice join of (G; x-y) and (G; -x-y) in abelian groups.  
Then mu(K)=1 and Nabla(K)=[1,omega).
	2. K = the lattice join of (G; x-y), (G; -x+y) and (G; -x-y) in  
abelian groups. Then mu(K)=1 and Nabla(K)=[1,omega).
	3. K = the variety of all Hilbert algebras. Then mu(K)=2 and Nabla(K) 
=[2,omega).
	4. K = the Kalman variety of subtractive algebras. Then mu(K)=2 and  
Nabla(K)=[2,omega).
	5. K = the variety of commutative BCK-algebras. Then mu(K)=2 and  
Nabla(K)=[2,omega).

Results 1 and 2 are obtained in collaboration with David Kelly.  
Results 3 and 5 are obtained in collaboration with Sergiu Rudeanu of  
University of Bucharest and result 4 on Kalman algebras is in  
collaboration with my graduate student Adam Gareau.

The invisible non-human collaborator in the proofs of all these  
theorems is, of course, Prover9. I will show how the program was  
influential in getting the minimum equational bases in the various  
examples mentioned above. I believe that the technique employed to  
make Prover9 discover new equations will be useful for tackling  
similar problems in other equational theories.
==========================================================