In automated deduction and automated proof transformation, one frequently deals with formal proofs that are not easily readable or understandable by humans. Two factors contributing to this problem are: 1) that real formal proofs are usually big; 2) that they are full of trivial (structural) inference steps. The key inference steps, of interest to the human reader, are thus hidden in the middle of the proof. In this work we provide solutions for this problem in the case of proofs in sequent caclulus LK for classical first-order logic. We analyze three pre-existing algorithms and we improve them by designing a fourth algorithm. The essential idea behind all four algorithms is the extraction of a Herbrand Sequent, which will shortly contain information about instantiations of quantified variables in the proof. In first-order logic, these instantiations correspond to the crucial and creative inference steps. Therefore, the extracted Herbrand Sequent summarizes the interesting content of the proof.