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]
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]
^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.