Son of BirdBrain

This page is obsolete. There is a new a much better version, Son of BirdBrain II, which uses Prover9 and Mace4.

With these pages you can construct some simple conjectures and run them through Otter and Mace2, two of Argonne's automated deduction systems.

Select an area from the following list, then click "OK".

Group Theory
Quasigroups and Loops
Ring Theory
Lattice Theory
CS Commutator
Boolean Algebras
The Robbins Problem
Combinatory Logic
Equivalential Calculus

Add your area to Son of BirdBrain's repertoire.

What's really going on here?

Created in 1996
Send comments to

These activities are projects of the Mathematics and Computer Science Division of Argonne National Laboratory.