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

Aboul-Hosn, Kamal; Kozen, Dexter

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

File(s)

TR2003-1906.ps (125.92 KB)

Permanent Link(s)

https://hdl.handle.net/1813/5619

Collections

Computing and Information Science Technical Reports

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

Keywords

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