T. Dunchev: "Simplification of Herbrand Sequents"; Supervisor: A. Leitsch; Institut für Computersprachen E185/2, 2009; final examination: 2009-09-09.