KAT-ML: An Interactive Theorem Prover for Kleene Algebra with Tests
MetadataShow full item record
Aboul-Hosn, Kamal; Kozen, Dexter
KAT-ML is 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. We describe the main features of the system and illustrate its use with some examples.
computer science; technical report
Previously Published As