Тема выпускной квалификационной работы: «Сравнительное исследование эффективности стратегий оптимизации метода резолюций c применением полиномиальной унификации Робинсона». Данная работа относится к сфере решения математических задач с помощью систем автоматического доказательства теорем и посвящена исследованию эффективности применения различных алгоритмов унификации в стратегиях оптимизации метода резолюций. В первой главе работы описывается применение систем автоматического доказательство теорем. Приводится обзор популярных систем для логики предикатов первого порядка. Во второй главе описывается математический аппарат метода резолюций, приводится теоретическое описание выбранных для исследования стратегий оптимизации и алгоритмов унификации. В третьей главе приведены особенности программной реализации разработанного приложения, с помощью которого проводился анализ. В четвертой главе выполнено сравнение эффективности использования исследуемых алгоритмов унификации в стратегиях оптимизации метода резолюций. На основании проведенного исследования наиболее эффективной из всех рассмотренных в работе процедур унификации оказалась полиномиальная модификация алгоритма Робинсона.

The subject of the graduate qualification work is «Comparative study of the efficiency of optimization resolution strategies using Robinson's polynomial unification». This work belongs to the field of solving mathematical problems using automatic theorem proving systems and is devoted to the study of the effectiveness of using various unification algorithms in optimization resolution strategies. The first chapter of the work describes the application of automatic theorem proving systems. An overview of popular systems for first-order predicate logic is also given. The second chapter describes the mathematical apparatus of the resolution method, provides a theoretical description of the optimization resolution strategies and unification algorithms selected for the study. The third chapter contains the features of the software implementation of the developed application, with the help of which the analysis was carried out. The fourth chapter compares the efficiency of using the studied unification algorithms in the optimization resolution strategies. Based on the study, a polynomial modification of the Robinson algorithm turned out to be the most effective of all the unification algorithms considered in the work.