V nastoyashchei rabote osushchstvlyaetsya vklyuchenie pravila binarnoi indukcii, opisannogo v [1], v avtomaticheskie procedury oproverzheniya v teoriyah pervogo poryadka. Privodit\-sya modificirovannyi algoritm unifikacii dlya otyskaniya podstanovki kotoraya potrebuet\-sya dlya primenjeniya pravila binarnoi indukcii. Rassmatrivaet\-sya algoritm poiska oproverzheniya s rezolyuciei i pravilom binarnoi indukcii v teoriyah pervogo poryadka s matematicheskoi indukciei. Privodit\-sya svedeniya o programmnoi sisteme i rezul'tatah otladki na evm.