ARA swMATH ID: 8504 Software Authors: Sinz, Carsten Description: 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. Homepage: http://www-sr.informatik.uni-tuebingen.de/~sinz/ARA/ Related Software: RALL; Ralf; RelView; Ynot; Coq; Mace4; Prover9; SPASS; Isabelle/HOL; ModLeanTAP; SICStus; LoTREC Cited in: 5 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year System description: ARA – an automatic theorem prover for relation algebras. Zbl 0963.68524Sinz, Carsten 2000 all top 5 Cited by 11 Authors 1 Berghammer, Rudolf 1 Formisano, Andrea 1 Gordeev, Lev 1 Höfner, Peter 1 Malecha, Gregory 1 Morrisett, Greg 1 Nicolosi Asmundo, Marianna 1 Shinnar, Avraham 1 Sinz, Carsten 1 Stucke, Insa 1 Wisnesky, Ryan Cited in 2 Serials 1 Annals of Pure and Applied Logic 1 Journal of Applied Non-Classical Logics Cited in 2 Fields 5 Computer science (68-XX) 3 Mathematical logic and foundations (03-XX) Citations by Year