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

Citations by Year