Queen's Logo

CISC422: Formal Methods in Software Engineering

Using Jape for Assignment 2

Intro

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.
  1. Start Jape
  2. In the "Jape Control" window, select "Open new theory..." under "File".
  3. We now have to load the logic. Open "I2L.jt" in folder "natural_deduction".
  4. 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.
  5. 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.
  6. 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").
  7. More info on how to use Jape can be found in this manual prepared by the author of Jape.
Last modified: Mon Sep 5 18:04:00 EDT 2019