We present a theorem proving system for abstract relation algebra called RALL (=Relation-Algebraic Language and Logic), based on the generic theorem prover Isabelle. On the one hand, the system is an advanced case study for Isabelle/HOL, and on the other hand, a quite mature proof assistant for research on the relational calculus. RALL is able to deal with the full language of heterogeneous relation algebra including higher-order operators and domain constructions, and checks the type-correctness of all formulas involved. It offers both an interactive proof facility, with special support for substitutions and estimations, and an experimental automatic prover. The automatic proof method exploits an isomorphism between relation-algebraic and predicate-logical formulas, relying on the classical universal-algebraic concepts of atom structures and complex algebras.
CITATION STYLE
von Oheimb, D., & Gritzner, T. F. (1997). RALL: Machine-Supported proofs for relation algebra. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1249, pp. 380–394). Springer Verlag. https://doi.org/10.1007/3-540-63104-6_36
Mendeley helps you to discover research relevant for your work.