KAT-ML: an interactive theorem prover for Kleene algebra with tests. We describe KAT-ML, an implementation of an interactive theorem prover for Kleene algebra with tests (KAT). The system is designed to reflect the natural style of reasoning with KAT that one finds in the literature. One can also use the system to reason about properties of simple imperative programs using schematic KAT (SKAT). We explain how the system works and illustrate its use with some examples, including an extensive scheme equivalence proof.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element