RALL: Machine-supported proofs for relation algebra. We present a theorem proving system for abstract relation algebra called RALL (=Relation-Algebraic Language and Logic), based on the generic theorem prover Isabelle. On the one hand, the system is an advanced case study for Isabelle/HOL, and on the other hand, a quite mature proof assistant for research on the relational calculus. RALL is able to deal with the full language of heterogeneous relation algebra including higher-order operators and domain constructions, and checks the type-correctness of all formulas involved. It offers both an interactive proof facility, with special support for substitutions and estimations, and an experimental automatic prover. The automatic proof method exploits an isomorphism between relation-algebraic and predicate-logical formulas, relying on the classical universal-algebraic concepts of atom structures and complex algebras.
Keywords for this software
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- Braibant, Thomas; Pous, Damien: Deciding Kleene algebras in Coq (2012)
- Guttmann, Walter: Typing theorems of omega algebra (2012)
- Foster, Simon; Struth, Georg; Weber, Tjark: Automated engineering of relational and algebraic methods in Isabelle/HOL (invited tutorial) (2011)
- Braibant, Thomas; Pous, Damien: An efficient Coq tactic for deciding Kleene algebras (2010)
- Formisano, Andrea; Nicolosi-Asmundo, Marianna: An efficient relational deductive system for propositional non-classical logics (2006)
- Sinz, Carsten: System description: ARA -- an automatic theorem prover for relation algebras (2000)
- Dawson, Jeremy E.; Goré, Rajeev: A mechanised proof system for relation algebra using display logic (1998)