Jape (software)
| Company type | Free software |
|---|---|
| Industry | Software, Education |
| Founded | 1992 |
| Founder | Richard Bornat, Bernard Sufrin |
| Headquarters | London, Oxford , United Kingdom |
| Products | Graphical proof assistant software |
| Owner | Queen Mary University of London, University of Oxford |
| Website | github |
Jape is a versatile graphical proof assistant created by Richard Bornat at Queen Mary, University of London and Bernard Sufrin at University of Oxford. Compatible with Macintosh, Unix, and Microsoft Windows operating systems, it is developed in Java and distributed under the terms of the GNU GPL license.
Widely regarded as a premier resource for teaching logic with computer assistance, Jape excels in facilitating exercises related to proofs within the field of mathematical logic.
History
Developed in 1992 by Bornat and Sufrin with the goal of improving comprehension of formal reasoning, the term "Jape" was introduced by Sufrin. The software transitioned to an open-source model on GitHub in 2019.
Overview
Jape allows users to explore and construct proofs interactively within logical frameworks defined by inference rules. It interprets user interactions—such as typing, clicking, or dragging—as proof operations that are rigorously validated by the embedded object logic. Users have the flexibility to insert or remove proof steps, while Jape continuously generates and presents the evolving proof tree in multiple visual formats to support strategic planning.
The program offers various abstraction layers and supports forward proofs using natural deduction through dedicated presentation modes. It also accommodates different forms of the sequent calculus and natural deduction, including proofs involving quantifiers.
See also
References
External links
- Jape Online official distribution portal
- Jape on SourceForge
- Jape repository on GitHub