ProjectProject
Jape is an interactive tool designed to help with learning, teaching and using formal reasoning. It takes a description of a logic as a system of inference rules, and provides support for the interactive development of proofs in that logic. It has a tactic language which is used to control the display of proofs and to perform searches. The syntax of logical formulae, the form of judgements, the rules used, the entries in menus, the effect on the proof each gesture -- all these are under the control of the person who encodes the logic.
Charles
Crighton