Otter 3.3 Theorem Prover
Mace 2.2 Finite Model Searcher
This directory contains the Otter 3.3 packages (including Mace 2.2)
for Unix-like and for Microsoft Windows operating systems.
Unix-like systems (including MacOS X)
Microsoft Windows
Another Way to Run Otter and Mace2
The standard packages above require you to run Otter and Mace2
from a command line (Terminal in Mac, Command Prompt in Windows).
If you don't like to use command lines, there is a simple
graphical interface to Otter and Mace2.
The Official Web Pages
William McCune
Mathematics and Computer Science Division
Argonne National Laboratory