| Original author(s) | Richard Bornat, Bernard Sufrin |
|---|---|
| Stable release | |
| Repository | github |
| Written in | OCaml,Java |
| Type | Proof assistant |
| License | GPL-2.0 license |
Jape is a configurable, graphicalproof assistant, originally developed byRichard Bornat atQueen Mary, University of London andBernard Sufrin theUniversity of Oxford.[2] The program is available for theMac,Unix, andWindows operating systems. It is written in theJava programming language and released under theGNU GPL.
It is claimed that Jape is the most popular program for "computer-assisted logic teaching" that involves exercises in developing proofs inmathematical logic.[3]
Jape was created in 1992 by Richard Bornat and Bernard Sufrin with the intent to get a better understanding of the formal reasoning. Bernard Sufrin came up with the name "Jape".[2]
In 2019, they released the code on GitHub.[4]
Jape supports human-directed discovery ofproofs in a logic which is defined by the user as a system ofinference rules. It maps the user's gestures (e.g. typing, mouse-clicks or mouse-drags) to the assistant's proof actions. Jape does not have any special knowledge of anyobject logic or theory, and it will make moves in a proof if and only if they are justifiable by rules of the object logic that is currently loaded.[5] Jape allows to make proof steps and undo them, and it shows the effect of the added proof steps which helps to understand strategies for finding proofs.[2]: 60 When the user adds and removes the proof steps, the proof tree is constructed which Jape can show either in a tree shape or in box forms.[5] Jape allows to display proofs at different levels of abstraction. It is also possible to present a forward proof in a natural deduction style by using the specialized modes of display for proofs.[6]
Jape works with variants of thesequent calculus andnatural deduction. It also supports formal proofs withquantifiers.[2]: 84