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

Anything in here will be replaced on browsers that support the canvas element