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.
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