Forbidden Theorems

Many results in algebra have the form: An algebra belongs to the class of algebras C if and only if it belong to the overclass D and does not contain some given subalgebras. 

Typical example: a lattice is distributive if and only if it does not contain the pentagon or the diamond. 

This tool finds Forbidden Structure Conjectures and will be a package for ProverX.


This is the kernel of the whole system. 

Produced with Yves Robert and Bob Veroff, this tool integrates several different packages for ATP.  

Semigroup Varieties

Given a finite semigroup, this tool tries to find a base of identities for the variety of semigroups it generates. 

Envery semigroup up to order 5, every group up to order 47, bands of arbitrary large order, and many other classes are currently supported. It will be a package for ProverX. 


One of the reasons Prover9 became so popular among mathematicians is its extremely user friendly syntax.

The drawback is that problems written in that syntax cannot be passed on to other ATP systems.


Translator for Prover9 proofs. 

Computer proofs are usually very difficult to follow and understand. This tool accepts Prover9 proofs (in the expanded format) and a particular proof line, and outputs a humanized proof. It will be a package for ProverX. 

Produced with José Duarte and Michael Kinyon.