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.

Produced with Michael Kinyon.