# 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}}
}