Jape
Original author(s)Richard Bornat, Bernard Sufrin
Stable release
9.1.8[1] / October 10, 2023 (2023-10-10)
Repositorygithub.com/RBornat/jape
Written inOCaml, Java
TypeProof assistant
LicenseGPL-2.0 license

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.

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

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

Jape's goal is to support human-directed discovery of proofs in a logic which is described beforehand as a system of inference rules. It allows to map the user's gestures (e.g. typing, mouse-clicks or mouse-drags) to the assistant's proof actions. Jape is designed to not have any special knowledge of any object logic or theory, thus 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 appropriate 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

References

  1. ↑ "Corrected proof completion (and fixed zombie proof windows)". GitHub. Retrieved January 11, 2024.
  2. 1 2 3 4 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.
  3. ↑ 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.
  4. ↑ "(Modified) first github release". GitHub. December 6, 2019. Retrieved January 11, 2024.
  5. 1 2 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.
  6. ↑ 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.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.