KAT-ML: An Interactive Theorem Prover for Kleene Algebra with Tests

Thumbnail
View/Open
PERMANENT LINK(S)
https://hdl.handle.net/1813/5619
Collections
Metadata
Show full item record
Author
Aboul-Hosn, Kamal; Kozen, Dexter
Abstract
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.
Date Issued
2003-08-21
Publisher
Cornell University
Subject
computer science; technical report
Previously Published As
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2003-1906
Type
technical report

Statistics