The possibility of quantified cut-introduction, which this thesis is dedicated to, offers the possiblity of compressing a proof in sequent calculus, to improve readability and provide interesting new insights into proof theory. The problem of introducing quantified cuts into a cut-free proof in sequent calculus is a quite complex procedure, which can be accomplished in various ways. The method described in this thesis realised this by applying several consecutive steps. First essential parts of the proof are extracted, namely the Herbrand sequent, from which a term language is generated. This term language represents all needed instantiations of quantified formulas and will be tried to be compressed by a minimal grammar. The problem of finding a minimal grammar for this language is achieved by reducing it to the MinCostSAT problem and thus generate it via the resulting interpretation. This grammar forms the base for the further construction of an extended Herbrand sequent, which again illustrates an intermediate step to build a proof with cuts. On the basis of  an algorithm was constructed performing this minimal grammar computation, which was tested via a large series of experiments. Although previously developed methods, capable of cut-introduction, were not outperformed by this new method, the methods were extended by the possibility of introducing not just one single-quantified cut, but multiple single-quantified cuts at once. Possible new insights may be gained by this implemented method, where simultaneously a small step towards cut-introduction for cuts with more complex cut-formulas was made.