With these pages you can construct some simple abstract algebra and logic problems and run them through Prover9, which searches for proofs, and Mace4, which searches for counterexamples.

*A New Feature:* In addition to selecting hypotheses and conclusions
from lists of formulas, you can compose your own.

This system is a successor to the
original *Son of BirdBrain*, which uses
Otter and
Mace2.

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

Send comments to William McCune