Formal proofs of interesting mathematical theorems are usually too large andfull of trivial structural information and hence hard to understand andanalyze. Tech... » 

Formal proofs of interesting mathematical theorems are usually too large andfull of trivial structural information and hence hard to understand andanalyze. Techniques to extract specific essential information from these proofsare needed. This book describes four algorithms to extract a Herbrand sequentof the endsequent of proofs written in Gentzens Sequent Calculus LK forclassical FirstOrder Logic. Within this calculus we define a Herbrand sequentas a generalization of Herbrand disjunction and its extraction can be used tosummarize the creative information of a formal proof which lies on theinstantiations chosen for the quantifiers. One of these algorithms has beenimplemented in CERes CutElimination by Resolution an automated system forproof transformations and analysis. «