| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 10329698 | Electronic Notes in Theoretical Computer Science | 2005 | 19 Pages |
Abstract
We propose diagrammatic techniques for visualizing relational reasoning in formal methods like B or Z; in particular for induction and coinduction. These are similar to those for functional diagrams in category theory and inspired by rewriting theory. Diagrams are endowed with a simple algebraic semantics that imposes a convenient balance between expressive and algorithmic power. This makes the approach particularly suitable for mechanization and automation. Its usefulness for visual reasoning is illustrated by various examples.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Michael Ebert, Georg Struth,