Summary
Jape is a configurable, graphical proof assistant, originally developed by Richard Bornat at Queen Mary, University of London and Bernard Sufrin the University of Oxford.[2] The program is available for the Mac, Unix, and Windows operating systems. It is written in the Java programming language and released under the GNU GPL.
| Original author(s) | Richard Bornat, Bernard Sufrin |
|---|---|
| Stable release | 9.1.8[1]
/ October 10, 2023 |
| Repository | github |
| Written in | OCaml, Java |
| Type | Proof assistant |
| License | GPL-2.0 license |
It is claimed that Jape is the most popular program for "computer-assisted logic teaching" that involves exercises in developing proofs in mathematical logic.[3]
History edit
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]
Overview edit
Jape supports human-directed discovery of proofs in a logic which is defined by the user as a system of inference 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 any object 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 the sequent calculus and natural deduction. It also supports formal proofs with quantifiers.[2]: 84
See also edit
References edit
- ^ "Corrected proof completion (and fixed zombie proof windows)". GitHub. Retrieved January 11, 2024.
- ^ a b c d Bornat, Richard (February 1, 2017). "Proof and Disproof in Formal Logic: An Introduction for Programmers" (PDF). Archived (PDF) from the original on April 18, 2022. Retrieved January 11, 2024.
- ^ Cezary Kaliszyk; Freek Wiedijk; Maxim Hendriks; Femke van Raamsdonk (2007). "Teaching logic using a state-of-the-art proof assistant" (PDF). H. Geuvers and P. Courtieu (Eds.), PATE'07, International Workshop on Proof Assistants and Types in Education: 37–50. Archived from the original (PDF) on January 17, 2023.
- ^ "(Modified) first github release". GitHub. December 6, 2019. Retrieved January 11, 2024.
- ^ a b Sufrin, Bernard; Bornat, Richard (April 3, 1998). "User Interfaces for Generic Proof Assistants Part I: Interpreting Gestures" (PDF). Archived (PDF) from the original on August 15, 2023. Retrieved January 11, 2024.
- ^ Sufrin, Bernard; Bornat, Richard (March 1998). "User Interfaces for Generic Proof Assistants Part II: Displaying Proofs" (PDF). Archived (PDF) from the original on January 11, 2024. Retrieved January 11, 2024.
External links edit
- Jape Online official distribution website
- Jape SourceForge portal
- Jape on Github