We give a general introduction to the problem of computation in groups and define logical graphs for formal proofs. Then, we present the notion of distorsion for finitely presented groups, and show how this phenomena is recaptured by the process of cut-elimination in formal proofs.