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