Jape is a configurable, graphical proof assistant, originally developed by Richard Bornat at

Queen Mary, University of London , mottoeng = With united powers , established = 1785 – The London Hospital Medical College1843 – St Bartholomew's Hospital Medical College1882 – Westfield College1887 – East London College/Queen Mary College , type = Public researc ...

and Bernard Sufrin the

University of Oxford , mottoeng = The Lord is my light , established = , endowment = £6.1 billion (including colleges) (2019) , budget = £2.145 billion (2019–20) , chancellor ...

. It allows user to define a

logic Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premise ...

, decide how to view proofs, and much more. It works with variants of the

sequent calculus In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautology i ...

and

natural deduction In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use ax ...

. It is claimedC. Kaliszyk, F. Wiedijk, M. Hendriks and F. van Raamsdonk,
Teaching logic using a state-of-the-art proof assistant
" In: H. Geuvers and P. Courtieu (eds.), ''PATE'07, International Workshop on Proof Assistants and Types in Education,'' 37–50, 2007. that Jape is the most popular program for "computer-assisted logic teaching" that involves exercises in developing proofs in

mathematical logic Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal ...

. The program is available for the Mac,

Unix Unix (; trademarked as UNIX) is a family of multitasking, multiuser computer operating systems that derive from the original AT&T Unix, whose development started in 1969 at the Bell Labs research center by Ken Thompson, Dennis Ritchie, an ...

, and

Windows Windows is a group of several proprietary graphical operating system families developed and marketed by Microsoft. Each family caters to a certain sector of the computing industry. For example, Windows NT for consumers, Windows Server for ser ...

operating systems. It is written in the

Java Java (; id, Jawa, ; jv, ꦗꦮ; su, ) is one of the Greater Sunda Islands in Indonesia. It is bordered by the Indian Ocean to the south and the Java Sea to the north. With a population of 151.6 million people, Java is the world's mos ...

programming language and released under the GNU GPL.

References

External links

Jape Online
official distribution website
Jape

SourceForge SourceForge is a web service that offers software consumers a centralized online location to control and manage open-source software projects and research business software. It provides source code repository hosting, bug tracking, mirroring ...

portal Proof assistants Free theorem provers {{software-stub

See also

References

External links