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 (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 RPC3 , RPC4 and RPC ω . aRa, our implementation in Haskell, offers different reduction strategies for RPC n , and a set of simplifications preserving n-variable provability.
This work was partially supported by DFG under grant Ku 966/4-1.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Chin, L.H., Tarski, A.: Distributive and modular laws in the arithmetic of relation algebras, vol. 1(9), pp. 341–384. University of California Publications in Mathematics, New Series, Berkeley, Los Angeles,santa barbara (1951)
J. Dawson and R. Gor_e. A mechanized proof system for relation algebra using display logic. In JELIA’98, LNAI 1489, pages 264{278. Springer, 1998.
Gordeev, L.: Cut free formalization of logic with finitely many variables, part I. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 136–150. Springer, Heidelberg (1995)
Gordeev, L.: Variable compactness in 1-order logic. Logic Journal of the IGPL 7(3), 327–357 (1999)
Hattensperger, C., Berghammer, R., Schmidt, G.: RALF - a relationalgebraic formula manipulation system and proof checker. In: AMAST 1995, Workshops in Computing, pp. 405–406. Springer, Heidelberg (1994)
Maddux, R.: A sequent calculus for relation algebras. Annals of Pure and Applied Logic 25, 73–101 (1983)
Tarski, A., Givant, S.: A Formalization of Set Theory without Variables. Optimization Techniques 1975, vol. 4. American Mathematical Society, Providence (1987)
von Oheimb, D., Gritzner, T.: RALL: Machine-supported proofs for relation algebra. In: McCune, W. (ed.) CADE 1997. LNCS(LNAI), vol. 1249, pp. 380–394. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sinz, C. (2000). System Description: aRa – An Automatic Theorem Prover for Relation Algebras. In: McAllester, D. (eds) Automated Deduction - CADE-17. CADE 2000. Lecture Notes in Computer Science(), vol 1831. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721959_13
Download citation
DOI: https://doi.org/10.1007/10721959_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67664-5
Online ISBN: 978-3-540-45101-3
eBook Packages: Springer Book Archive