Installing Prover9, Mace4, and Friends

Linux and macOS

The following commands are run in a terminal window. On macOS, open Terminal (found in Applications → Utilities, or press Cmd+Space and search for "Terminal").

macOS only: If you have not previously installed the Xcode command line tools, run the following command first. A dialog will appear — click "Install" and wait for it to finish.

xcode-select --install

Visit the Prover9 Web page and download the current version of LADR. The filename should be something like Prover9-LADR-2026-4F.tar.gz; make sure that file is in your current directory. Run the following commands.

tar xzf Prover9-LADR-2026-4F.tar.gz
cd Prover9-LADR-2026-4F
make all

Prover9, Mace4, Prooftrans, and several other programs should now be in the directory Prover9-LADR-2026-4F/bin. You can either include that directory in your search path or copy those programs to some directory that is already in your search path.

Microsoft Windows (WSL)

Prover9 runs on Windows through the Windows Subsystem for Linux (WSL).

1. Install WSL

Open PowerShell as Administrator (right-click the Start button → "Terminal (Admin)" or search for "PowerShell" and choose "Run as administrator"), then run:

wsl --install

This installs WSL with Ubuntu by default. Restart your computer when prompted.

2. Set Up Ubuntu

After restarting, open the Ubuntu app from the Start menu. On first launch it will ask you to create a username and password. Then install the build tools:

sudo apt update
sudo apt install build-essential

3. Download and Build

Still in the Ubuntu terminal, download and build Prover9:

wget https://github.com/AlgorithmicTruth/Prover9/archive/refs/tags/LADR-2026-4F.tar.gz
tar xzf Prover9-LADR-2026-4F.tar.gz
cd Prover9-LADR-2026-4F
make all

The programs will be in the Prover9-LADR-2026-4F/bin directory.

Note: Your Windows files are accessible from WSL at /mnt/c/Users/YourName/, so you can run Prover9 on input files stored on your Windows desktop.