On Automating the Calculus of Relations

9 years 2 months ago
On Automating the Calculus of Relations
Relation algebras provide abstract equational axioms for the calculus of binary relations. They name an established area of mathematics with various applications in computer science. We prove more than hundred theorems of relation algebras with off-the-shelf automated theorem provers. This yields a basic calculus from which more advance applications can be explored. Here, we present two examples from the formal methods literature. Our experiments not only further underline the feasibility of automated deduction in complex algebraic structures and provide theorem proving benchmarks, they also pave the way for lifting established formal methods such as B or Z to a new level of automation.
Georg Struth, Peter Höfner
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where CADE
Authors Georg Struth, Peter Höfner
Comments (0)