Jape (software)
{{Short description|Proof assistant program}}
{{infobox software
| repo = {{url|https://github.com/RBornat/jape}}
| programming language = OCaml, Java
| license = GPL-2.0 license
| latest release version = 9.1.8{{cite web |url=https://github.com/RBornat/jape/releases/tag/9.1.8 |title=Corrected proof completion (and fixed zombie proof windows) |website=GitHub |access-date=January 11, 2024}}
| latest release date = {{Start date and age|2023|10|10}}
| author = Richard Bornat, Bernard Sufrin
| genre = Proof assistant
}}
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.{{cite web |url=https://homepages.phonecoop.coop/randj/richard/books/ProofandDisproof.pdf |title=Proof and Disproof in Formal Logic: An Introduction for Programmers |first=Richard |last=Bornat |author-link=Richard Bornat |date=February 1, 2017 |access-date=January 11, 2024 |archive-url=https://web.archive.org/web/20220418220535/https://homepages.phonecoop.coop/randj/richard/books/ProofandDisproof.pdf |archive-date=April 18, 2022 |url-status=live}} 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.
It is claimed that Jape is the most popular program for "computer-assisted logic teaching" that involves exercises in developing proofs in mathematical logic.{{cite journal |url=http://www.cs.vu.nl/~femke/ps/formed08.pdf |title=Teaching logic using a state-of-the-art proof assistant |journal=H. Geuvers and P. Courtieu (Eds.), PATE'07, International Workshop on Proof Assistants and Types in Education |author1=Cezary Kaliszyk |author2=Freek Wiedijk |author3=Maxim Hendriks |author4=Femke van Raamsdonk |year=2007 |pages=37–50 |archive-url=https://web.archive.org/web/20230117044342/https://www.cs.vu.nl/~femke/ps/formed08.pdf |archive-date=January 17, 2023 |url-status=dead}}
History
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".{{r|thebook}}
In 2019, they released the code on GitHub.{{cite web |url=https://github.com/RBornat/jape/releases/tag/9.0.8 |title=(Modified) first github release |website=GitHub |date=December 6, 2019 |access-date=January 11, 2024}}
Overview
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.{{cite web |url=https://www.cs.ox.ac.uk/people/bernard.sufrin/jape.org.uk/DOCUMENTS/CURRENT/UITP96-1.pdf |title=User Interfaces for Generic Proof Assistants Part I: Interpreting Gestures |first1= Bernard |last1=Sufrin |first2=Richard |last2=Bornat |date=April 3, 1998 |access-date=January 11, 2024 |archive-url=https://web.archive.org/web/20230815012405/https://www.cs.ox.ac.uk/people/bernard.sufrin/jape.org.uk/DOCUMENTS/CURRENT/UITP96-1.pdf |archive-date=August 15, 2023 |url-status=live}} 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.{{r|thebook|p=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.{{r|part1}} 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.{{cite web |url=http://www.cs.ox.ac.uk/people/bernard.sufrin/jape.org.uk/DOCUMENTS/OLD/UITP96-2.pdf |title=User Interfaces for Generic Proof Assistants Part II: Displaying Proofs |first1= Bernard |last1=Sufrin |first2=Richard |last2=Bornat |date=March 1998 |access-date=January 11, 2024 |archive-url=https://web.archive.org/web/20240111225629/http://www.cs.ox.ac.uk/people/bernard.sufrin/jape.org.uk/DOCUMENTS/OLD/UITP96-2.pdf |archive-date=January 11, 2024 |url-status=live}}
Jape works with variants of the sequent calculus and natural deduction. It also supports formal proofs with quantifiers.{{r|thebook|p=84}}
See also
References
External links
- [http://japeforall.org.uk Jape Online] official distribution website
- [http://sourceforge.net/projects/jape/ Jape] SourceForge portal
- [https://github.com/RBornat/jape Jape on Github]
Category:Free software programmed in Java (programming language)