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.
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- 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)