Otter is a program that searches for proofs of statements in first-order logic with equality.
Mace2 is a program that searches for small (finite) models or counterexamples of the same kind of statement.
The conjectures you construct with Son of BirdBrain are given to Otter, which tries for a few seconds to find a proof. If Otter fails, the conjecture is given to Mace2, which searches for small counterexamples.
You can't really do much serious work with Son of BirdBrain, because (1) the set of formulas is fixed, (2) we can't give you more than a few seconds of search time, and (3) it uses Otter's automatic mode. But, once you're hooked, it's easy to get your own copy of Otter for your UNIX, Macintosh, or Microsoft computer.
Comments and questions can be sent to [email protected]. Also, it's easy to add new areas to Son of BirdBrain's repertoire.
(We know that the proofs and counterexamples aren't pretty---maybe someday ...)
Information on other automated deduction systems.
These activities are projects of the Mathematics and Computer Science Division of Argonne National Laboratory.