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.
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.
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.
