KAT-ML: an interactive theorem prover for Kleene algebra with tests

Journal of Applied Non-Classical Logics（2006）

引用 30|浏览6

暂无评分

摘要

Abstract: We describe an implementation of an interactive theorem prover forKleene algebra with tests (KAT). The system is designed to reflect the naturalstyle of reasoning with KAT that one finds in the literature. We illustrate itsuse with some examples.

查看译文

关键词

theorem provers,mathematical knowledge management.,program verification,kleene algebra,computer science,mathematical knowledge management,technical report,theorem prover

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要