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.