On rewriting behavioural semantics in process algebras

This paper concerns a verification system for process algebras formalisms based entirely on equational reasoning. One aspect of the kind of reasoning we want to do, the so-called automatic reasoning, that is, the possibility of equipping the axiomatic presentations of various behavioural equivalences with equivalent rewriting relations is analyzed. The problems and the adopted solutions to deal with observational congruence are discussed.