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.

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Georg Struth, Peter Höfner
• Keywords: Automated Reasoning, CADE 2008, Off-the-shelf Automated Theorem, Relation Algebras, Theorem Proving Benchmarks