Magistriniame darbe ,,Formulių redukcija multiplikatyvioje aritmetikoje” nagrinėjamas sekvencinis multiplikatyvios aritmetikos variantas su lygybe. Šis skaičiavimas yra bazė, kuriant skaičiavimus,naudojamus automatizuojant įrodymus įvairiuose aritmetikos fragmentuose. Darbo tikslas- susipažinti su įrodymo teorija bei jos taikymu sekvenciniame multiplikatyviosios aritmetikos variante.Darbas padalintas į 3 skyrius : pargindinės sąvokos, pagalbinės lemos ir formulių redukcija. Pradžioje pateikiamas trumpas įvadas į Peano aritmetiką.Apibrėžiamas sekvencinis skaičiavimas K, turintis neloginių simbolių signatūrą {0,',P, *,=}.Savarankišką darbo dalį sudaro antrasis bei trečiasis skyriai.Bet kuriai bekvantorinei skaičiavimo K formulei A(x) randama tam tikros formos jai ekvivalenti normalioji disjunkcinė forma.Taip pat nagrinėjama sutvarkytųjų formulių redukcija. / In this postgraduate work “Reduction of formulas in the multiplicative arithmetic” the sequential variant with equality of multiplicative arithmetic is being analyzed. This calculus is a base when creating calculations which are used in different fragments of arithmetic. The aim of this work is to get acquainted with a proving theory and its application in sequential variant of multiplicative arithmetic. The work is divided into 3 sections: main conceptions, auxiliary lemmas and formula’s reduction. The short introduction into Pean’s arithmetic is given in the beginning. The sequential calculus K, which has non-logical symbol’s signature {0,`,P,.,=} is being described. Sections 2 and 3 are self-sufficient parts of this work. For any formula A(x) of calculation K the equivalent normal disjunctive form is found. Also the reduction of ordered formulas is analyzed.