Relation algebras provide abstract equational axioms for the calculus of binary relations. They name an established area of mathematics and have found numerous applications in computing. We prove more than hundred theorems of relation algebras with off-the-shelf automated theorem provers. They form a basic calculus from which more advanced applications can be explored. We also present two automation experiments from the formal methods literature. Our results further demonstrate the feasibility of automated deduction with complex algebraic structures. They also open a new perspective for automated deduction in relational formal methods. © 2008 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Höfner, P., & Struth, G. (2008). On automating the calculus of relations. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5195 LNAI, pp. 50–66). https://doi.org/10.1007/978-3-540-71070-7_5
Mendeley helps you to discover research relevant for your work.