Son of BirdBrain II

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

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

Contribute new areas to Son of BirdBrain II's repertoire.