Abstrakt. aRa är en automatisk teoremprovare för olika typer av relation algebras. Den är baserad på Gordeevs Reduction Predicate Calculi för n-variabel logik (RPCn) som tillåter första ordningens finita variabla bevis. Med hjälp av resultat från Tarski/Givant och Maddux kan vi bevisa giltighet i teorierna om enkel semi-associativ relation algebras, relation algebras och representativ relation algebras med hjälp av calculi RPC3, RPC4 och RPC. aRa, vårt genomförande i Haskell, erbjuder olika minskningsstrategier för RPCn, och en uppsättning förenklingar som bevarar n-variabel bevisbarhet.
ARA REF (Automatic Theorem prover for Relational Algebras) är en annan bevisassistent för relationella algebras.
System Description: aRa - An Automatic Theorem Prover for Relation Algebras
{'venue': 'Automated Deduction CADE-17, LNAI 1831', 'journal': None, 'mag_field_of_study': ['Computer Science']}