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
References in zbMATH (referenced in 5 articles , 1 standard article )
Showing results 1 to 5 of 5.
- Berghammer, Rudolf; Höfner, Peter; Stucke, Insa: Automated verification of relational while-programs (2014)
- Malecha, Gregory; Morrisett, Greg; Shinnar, Avraham; Wisnesky, Ryan: Toward a verified relational database management system (2010)
- Formisano, Andrea; Nicolosi-Asmundo, Marianna: An efficient relational deductive system for propositional non-classical logics (2006)
- Gordeev, L.: Finite methods in 1-order formalisms (2002)
- Sinz, Carsten: System description: ARA -- an automatic theorem prover for relation algebras (2000)