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 )
Showing results 1 to 5 of 5.
- 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)
- Nuka, Gift; Woodcock, Jim: Mechanising the alphabetised relational calculus. (2004)
- Gordeev, L.: Finite methods in 1-order formalisms (2002)
- Sinz, Carsten: System description: ARA -- an automatic theorem prover for relation algebras (2000)