RALF — A Relation-Algebraic Formula Manipulation System and Proof Checker. In the last years, relational calculus of Tarski and his co-workers has widely been used by computer scientists who view it as a convenient formalism for describing fundamental concepts of programming languages. Among other things, this was motivated by the simple component-free and “linear” nature of the relational formulae and terms which allows formal and often very concise manipulations. As has been demonstrated in a lot of articles, this makes programs and their properties more handy for theoretical investigations e.g., concerning proofs of transformation rules or verification rules.
Keywords for this software
References in zbMATH (referenced in 6 articles )
Showing results 1 to 6 of 6.
- Berghammer, Rudolf; Höfner, Peter; Stucke, Insa: Automated verification of relational while-programs (2014)
- Berghammer, Rudolf; Winter, Michael: Gunther Schmidt’s life as a mathematician and computer scientist (2014)
- Berghammer, Rudolf; Schmidt, Gunther; Winter, Michael: RelView and Rath -- two systems for dealing with relations. (2003)
- de Swart, Harrie (ed.); Orłowska, Ewa (ed.); Schmidt, Gunther (ed.); Roubens, Marc (ed.): Theory and applications of relational structures as knowledge instruments. COST Action 274, TARSKI. Revised papers (2003)
- Sinz, Carsten: System description: ARA -- an automatic theorem prover for relation algebras (2000)
- von Oheimb, David; Gritzner, Thomas F.: RALL: machine-supported proofs for relation algebra (1997)