System Description: ARA - An Automatic Theorem Prover for Relation Algebras

Abstract. 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 (RPCn) 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 RPC3, RPC4 and RPCω. aRa, our implementation in Haskell, offers different reduction strategies for RPCn, and a set of simplifications preserving n-variable provability.

• Type: Conference
• Year: 2000
• Where: CADE
• Authors: Carsten Sinz
• Keywords: CADE 2000, Logical Reasoning, Relation Algebras, Representable Relation Algebras, Semi-associative Relation Algebras