Conference
Calculational Relation-Algebraic Proofs in Isabelle/Isar
Abstract
We propose a collection of theories in the proof assistant Isabelle/Isar that support calculational reasoning in and about heterogeneous relational algebras and Kleene algebras.
Authors
Kahl W
Series
Lecture Notes in Computer Science
Volume
3051
Pagination
pp. 178-190
Publisher
Springer Nature
Publication Date
2004
DOI
10.1007/978-3-540-24771-5_16
Conference proceedings
Lecture Notes in Computer Science
ISSN
0302-9743