System description: ARA -- 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. Employing 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 ω . ARA, our irnplementation in Haskell, offers different reduction strategies for RPC n and a set of simplifications preserving n-variable provability.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element