Publication


RALL: Machine-supported Proofs for Relation Algebra

Conference on Automated Deduction -- CADE-14


Author: David von Oheimb, Thomas F. Gritzner
Year: 1997
Publisher: Springer LNCS 1249
Editor: William McCune
Abstract: 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.


Copyright © 1997 Springer-Verlag.
This paper is published by Springer LNCS.
Pre-print version available as compressed Postscript and PDF file. Slides  Isabelle sources


BibTeX entry:

@inproceedings {RALL_CADE-14, author = {Oheimb, David von and Thomas F. Gritzner}, title = {{RALL}: Machine-supported Proofs for Relation Algebra}, booktitle = {Conference on Automated Deduction -- CADE-14}, year = {1997}, editor = {William McCune}, publisher = {Springer}, series = {LNCS}, volume = {1249}, pages = {380--394}, abstract = {We present a theorem proving system for abstract relation algebra called RALL (= Relation-Algebraic Language and Logic), based on the generic theorem rover 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.}, url = {\url{http://ddvo.net/papers/RALL.html}} }