Jape is a configurable, graphical

proof assistant In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor ...

, originally developed by

Richard Bornat Richard Bornat (born 1944), is a British author and researcher in the field of computer science. He is also professor of Computer programming at Middlesex University. Previously he was at Queen Mary, University of London. Research Bornat's rese ...

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 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. It allows user to define a logic, decide how to view proofs, and much more ...

the

University of Oxford The University of Oxford is a collegiate research university in Oxford, England. There is evidence of teaching as early as 1096, making it the oldest university in the English-speaking world and the world's second-oldest university in contin ...

. 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 premis ...

, 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 ...

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 a ...

. 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 Mac or MAC most commonly refers to: * Mac (computer), a family of personal computers made by Apple Inc. * Mackintosh, a raincoat made of rubberized cloth * A variant of the word macaroni, mostly used in the name of the dish mac and cheese * 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, a ...

, 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 ...

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 mo ...

programming language and released under the

GNU GPL The GNU General Public License (GNU GPL or simply GPL) is a series of widely used free software licenses that guarantee end users the four freedoms to run, study, share, and modify the software. The license was the first copyleft for general ...

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, mirrori ...

portal Proof assistants Free theorem provers {{software-stub

See also

References

External links