The calculus of relations was introduced by Alfred Tarski, in an attempt to axiomatize the theory of binary relations, without dealing with individuals (the objects being related). It has also been called "relation algebras". Ten years ago, Doornbos, Backhouse and van der Woude [1997] showed that we can characterize the notion of a well-founded relation in a similar setting, so that we end up with the ability to reason by well-founded induction at this relatively high level of abstraction.

This setting is very well suited to the analysis of (semi) commutation properties (e.g., Newman's Lemma). In particular, we use it to obtain a new commutation property, which in turn can be used in order to obtain up-to techniques for bisimulation (the coinductive proof method commonly found in concurrency theory).