Assignment 2 asks you to use the theorem prover Jape from Oxford.
Jape supports a number of different logics each with their
own symbols and proof rules. You can even define your own
logic. For Assignment 2, however, we won't need all that
generality. We just want to use Jape to support us in
doing our propositional and predicate logic proofs.
Where to run Jape
Jape is installed in CASLAB, but you can also download it for free
and run it on your home machine. Jape is implemented in Java and
runs on Windows, Mac, and Linux. All you need is
Sun's JDK or JRE, version 1.8 or later.
The Jape site
contains the distribution (even with the source code), installation
instructions, and a documentation. Installation is very straightforward.
How to run Jape
Here's what you need to do for the assignment.
Start Jape
In the "Jape Control" window, select "Open new theory..." under "File".
We now have to load the logic. Open "I2L.jt" in folder
"natural_deduction".
Three windows should open up with conjectures, i.e., sequents in propositional and
predicate logic that have not been proven yet.
The sequents that the assignment asks you to prove may be appear in one of these
conjecture windows.
Selecting any of these conjectures will bring
up a proof window showing an incomplete proof
with the premises at the top and the conclusion
at the bottom. Proof rules can found under the "Backward" and
"Forward" tabs. Selecting a rule (typically after also selecting the
formula(s) that the rule should be applied to) will apply it to
your partial proof.
For the assignment, you may want to input your own sequent. To this end,
click "New..." in the "Conjectures" window to input a new sequent.
Note that any atomic propositions and predicate symbols
in the sequent that you input must begin with
"A", "B", "C", "E", "F", "G", "H",
"P", "R", "S", or "T".
Also, you must use "i", "j", "k", "x", "y", or "z" as variables.
Once your proof is complete, you can
save it (under tab "File").
Clicking "Done" (under tab "Edit") will close the proof window and
mark the conjecture as proven
in the "Conjectures" panel. You can also export an image of the proof
in postscript for printing (use "Export Proof" under tab "File").
More info on how to use Jape can be found in
this manual prepared by the author of Jape.