Kaisar Structured Proof Language


Proof assistants hold great promise for giving us certainty where certainty is needed, but their drawback has always been the difficulty of learning and using them, reducing productivity even for experienced users. One way to address this is by targeting an interface between the user and prover, such as the proof scripting language. The Isar structured proof language for higher-order logics, part of Isabelle, struck on a style of proof that significantly improves the readability and maintainability of proofs in higher-order logic.

However, not all logics are higher-order logics. In particular, we use a dynamic logic called differential dynamic logic to verify hybrid systems in KeYmaera X. Thus, the goal of Kaisar is to take the gains made by Isar and extend them with new insights specific to dynamic logic in order to provide the same convenience for dynamic logics that Isar provides for higher-order logics.

Example Proof in Experimental Kaisar Syntax

Related Publication(s)

Brandon Bohrer and André Platzer.
Kaisar: Structured Proofs for Dynamic Logics.
Draft. Available upon request.