In questo incontro studieremo come le combinatorial proofs di Hughes possono essere utilizzate per definire una nozione di equivalenza tra dimostrazioni per la logica classica. Mostreremo poi come diversi formalismi (calcolo dei sequenti, alberi di refutazione e resolution) possano essere tradotti in combinatorial proofs e quale nozione di identità viene definita da ciascuno di essi.