otter

Theorem prover and finite model searcher

Otter is an automated deduction system (theorem prover) for first-order logic with equality developed at Argonne National Laboratories.