An Automatic Theorem Prover for Relation Algebras

ARA is an automatic theorem prover for various kinds of relation algebras. It is based on Gordeev's Reduction Predicate Calculi for n-variable logic (RPC_n) which allow first-order finite variable proofs. Using results from Tarski/Givant and Maddux we can prove validity in the theories of simple semi-associative relation algebras, relation algebras and representable relation algebras using the calculi RPC_3, RPC_4 and RPC_w. ARA is a Haskell-implementation that offers various reduction strategies for RPC_n, and a set of simplifications preserving n-variable provability.


The ARA prover is currently only available as a binary distribution for Solaris on the SPARC architecture and for Windows NT.

Download Solaris version   (gzip)
Download WindowsNT version   (zip)


RA input language description   (PS version)

Besides this short input language description, there is no on-line documentation available so far. If you have any questions, feel free to contact the author.

(c) Carsten Sinz, January 2000