From Formulae to Rewriting Systems