Using Prover9

We will use prover9, a state-of-the-art resolution theorem prover for the next homework.

Prover9 can be run on a linux machine and you may use the linux cluster of Computer Science Department at (linux.cs.uiowa.edu).

You should have a linux account there and may use Bitvise SSH Client or PuTTY to access the cluster.

Once you are on a linux machine, you may download an executable of prover9 for linux, such as prover9.exe (if you are on the linux machine, you may use the command

    cp -p ~hzhang/.public-html/c188/prover9.exe .
to copy it to your current directory), or build one from the source code of prover9 . You may need to run
    chmod a+x prover9.exe
on linux before running prover9.exe. You can run this version of prover9 as
    ./prover9.exe < steam.in > steam.out
where steam.in is an input file for prover9 and steam.out is the output file of prover9.

You may also use the GUI version of prover9 and mace4 (available for both windows 10 and macintosh).

You can download The manual and examples of prover9 and mace4 if you run into problems using prover9/mace4.