automated deduction system
Otter is an automated theorem prover for first-order and equational logic, and Mace2 searches for finite models and counterexamples. Otter/Mace2 are no longer being actively developed, and maintenance and support minimal. We recommend using Otter/Mace2's successor Prover9/Mace4 instead.
released on 1 August 2004
|License||Verified by||Verified on||Notes|
|License:SimplePermissive||Deborah Nicholson||24 June 2008|
Leaders and contributors
Resources and communication
This entry (in part or in whole) was last reviewed on 20 January 2017.