Jape is a configurable proof calculator and supports the interactive discovery of formal proofs in inference systems. It is distributed with a number of example logic encodings: in particular a natural deduction, several sequent calculi, a treatment of Burroughs-Abadi-Newman protocols, a Hindley-Milner typing mechanism, and various others including even Aristotlean syllogisms. A manual (Roll your own Jape logic) is available for those who would like to experiment with their own encodings.
Get releases via the release page, and please report problems via the issues page.
Richard Bornat 2022/01/03