title: Ð¡ÑÐ°Ð²Ð½Ð¸ÑÐµÐ»ÑÐ½Ð¾Ðµ Ð¸ÑÑÐ»ÐµÐ´Ð¾Ð²Ð°Ð½Ð¸Ðµ ÑÑÑÐµÐºÑÐ¸Ð²Ð½Ð¾ÑÑÐ¸ ÑÑÑÐ°ÑÐµÐ³Ð¸Ð¹ Ð¾Ð¿ÑÐ¸Ð¼Ð¸Ð·Ð°ÑÐ¸Ð¸ Ð¼ÐµÑÐ¾Ð´Ð° ÑÐµÐ·Ð¾Ð»ÑÑÐ¸Ð¹ c Ð¿ÑÐ¸Ð¼ÐµÐ½ÐµÐ½Ð¸ÐµÐ¼ Ð¿Ð¾Ð»Ð¸Ð½Ð¾Ð¼Ð¸Ð°Ð»ÑÐ½Ð¾Ð¹ ÑÐ½Ð¸ÑÐ¸ÐºÐ°ÑÐ¸Ð¸ Ð Ð¾Ð±Ð¸Ð½ÑÐ¾Ð½Ð°
title: Ð²ÑÐ¿ÑÑÐºÐ½Ð°Ñ ÐºÐ²Ð°Ð»Ð¸ÑÐ¸ÐºÐ°ÑÐ¸Ð¾Ð½Ð½Ð°Ñ ÑÐ°Ð±Ð¾ÑÐ° Ð¼Ð°Ð³Ð¸ÑÑÑÐ°
titleType: Subtitle
title: Comparative study of the efficiency of optimization resolution strategies using Robinson's polynomial unification
Creators: name: ÐÐµÐ´Ð¾Ð², ÐÐ»ÐµÐºÑÐµÐ¹
Publisher: name: Ð¡Ð°Ð½ÐºÑ-ÐÐµÑÐµÑÐ±ÑÑÐ³ÑÐºÐ¸Ð¹ Ð¿Ð¾Ð»Ð¸ÑÐµÑÐ½Ð¸ÑÐµÑÐºÐ¸Ð¹ ÑÐ½Ð¸Ð²ÐµÑÑÐ¸ÑÐµÑ ÐÐµÑÑÐ° ÐÐµÐ»Ð¸ÐºÐ¾Ð³Ð¾
Year: 2021
Subjects: ÐÑÑÐ¸ÑÐ»Ð¸ÑÐµÐ»ÑÐ½ÑÐµ Ð¼Ð°ÑÐ¸Ð½Ñ ÑÐ»ÐµÐºÑÑÐ¾Ð½Ð½ÑÐµ
ÐÐ°ÑÐµÐ¼Ð°ÑÐ¸ÑÐµÑÐºÐ°Ñ ÑÐ¸Ð·Ð¸ÐºÐ°
Ð¼ÐµÑÐ¾Ð´ ÑÐµÐ·Ð¾Ð»ÑÑÐ¸Ð¹
Ð°Ð²ÑÐ¾Ð¼Ð°ÑÐ¸ÑÐµÑÐºÐ¾Ðµ Ð´Ð¾ÐºÐ°Ð·Ð°ÑÐµÐ»ÑÑÑÐ²Ð¾ ÑÐµÐ¾ÑÐµÐ¼
ÑÑÑÐ°ÑÐµÐ³Ð¸Ñ Ð¾Ð¿ÑÐ¸Ð¼Ð¸Ð·Ð°ÑÐ¸Ð¸
Ð°Ð»Ð³Ð¾ÑÐ¸ÑÐ¼ ÑÐ½Ð¸ÑÐ¸ÐºÐ°ÑÐ¸Ð¸

description: Ð¢ÐµÐ¼Ð° Ð²ÑÐ¿ÑÑÐºÐ½Ð¾Ð¹ ÐºÐ²Ð°Ð»Ð¸ÑÐ¸ÐºÐ°ÑÐ¸Ð¾Ð½Ð½Ð¾Ð¹ ÑÐ°Ð±Ð¾ÑÑ: Â«Ð¡ÑÐ°Ð²Ð½Ð¸ÑÐµÐ»ÑÐ½Ð¾Ðµ Ð¸ÑÑÐ»ÐµÐ´Ð¾Ð²Ð°Ð½Ð¸Ðµ ÑÑÑÐµÐºÑÐ¸Ð²Ð½Ð¾ÑÑÐ¸ ÑÑÑÐ°ÑÐµÐ³Ð¸Ð¹ Ð¾Ð¿ÑÐ¸Ð¼Ð¸Ð·Ð°ÑÐ¸Ð¸ Ð¼ÐµÑÐ¾Ð´Ð° ÑÐµÐ·Ð¾Ð»ÑÑÐ¸Ð¹ c Ð¿ÑÐ¸Ð¼ÐµÐ½ÐµÐ½Ð¸ÐµÐ¼ Ð¿Ð¾Ð»Ð¸Ð½Ð¾Ð¼Ð¸Ð°Ð»ÑÐ½Ð¾Ð¹ ÑÐ½Ð¸ÑÐ¸ÐºÐ°ÑÐ¸Ð¸ Ð Ð¾Ð±Ð¸Ð½ÑÐ¾Ð½Ð°Â». ÐÐ°Ð½Ð½Ð°Ñ ÑÐ°Ð±Ð¾ÑÐ° Ð¾ÑÐ½Ð¾ÑÐ¸ÑÑÑ Ðº ÑÑÐµÑÐµ ÑÐµÑÐµÐ½Ð¸Ñ Ð¼Ð°ÑÐµÐ¼Ð°ÑÐ¸ÑÐµÑÐºÐ¸Ñ Ð·Ð°Ð´Ð°Ñ Ñ Ð¿Ð¾Ð¼Ð¾ÑÑÑ ÑÐ¸ÑÑÐµÐ¼ Ð°Ð²ÑÐ¾Ð¼Ð°ÑÐ¸ÑÐµÑÐºÐ¾Ð³Ð¾ Ð´Ð¾ÐºÐ°Ð·Ð°ÑÐµÐ»ÑÑÑÐ²Ð° ÑÐµÐ¾ÑÐµÐ¼ Ð¸ Ð¿Ð¾ÑÐ²ÑÑÐµÐ½Ð° Ð¸ÑÑÐ»ÐµÐ´Ð¾Ð²Ð°Ð½Ð¸Ñ ÑÑÑÐµÐºÑÐ¸Ð²Ð½Ð¾ÑÑÐ¸ Ð¿ÑÐ¸Ð¼ÐµÐ½ÐµÐ½Ð¸Ñ ÑÐ°Ð·Ð»Ð¸ÑÐ½ÑÑ Ð°Ð»Ð³Ð¾ÑÐ¸ÑÐ¼Ð¾Ð² ÑÐ½Ð¸ÑÐ¸ÐºÐ°ÑÐ¸Ð¸ Ð² ÑÑÑÐ°ÑÐµÐ³Ð¸ÑÑ Ð¾Ð¿ÑÐ¸Ð¼Ð¸Ð·Ð°ÑÐ¸Ð¸ Ð¼ÐµÑÐ¾Ð´Ð° ÑÐµÐ·Ð¾Ð»ÑÑÐ¸Ð¹. Ð Ð¿ÐµÑÐ²Ð¾Ð¹ Ð³Ð»Ð°Ð²Ðµ ÑÐ°Ð±Ð¾ÑÑ Ð¾Ð¿Ð¸ÑÑÐ²Ð°ÐµÑÑÑ Ð¿ÑÐ¸Ð¼ÐµÐ½ÐµÐ½Ð¸Ðµ ÑÐ¸ÑÑÐµÐ¼ Ð°Ð²ÑÐ¾Ð¼Ð°ÑÐ¸ÑÐµÑÐºÐ¾Ð³Ð¾ Ð´Ð¾ÐºÐ°Ð·Ð°ÑÐµÐ»ÑÑÑÐ²Ð¾ ÑÐµÐ¾ÑÐµÐ¼. ÐÑÐ¸Ð²Ð¾Ð´Ð¸ÑÑÑ Ð¾Ð±Ð·Ð¾Ñ Ð¿Ð¾Ð¿ÑÐ»ÑÑÐ½ÑÑ ÑÐ¸ÑÑÐµÐ¼ Ð´Ð»Ñ Ð»Ð¾Ð³Ð¸ÐºÐ¸ Ð¿ÑÐµÐ´Ð¸ÐºÐ°ÑÐ¾Ð² Ð¿ÐµÑÐ²Ð¾Ð³Ð¾ Ð¿Ð¾ÑÑÐ´ÐºÐ°. ÐÐ¾ Ð²ÑÐ¾ÑÐ¾Ð¹ Ð³Ð»Ð°Ð²Ðµ Ð¾Ð¿Ð¸ÑÑÐ²Ð°ÐµÑÑÑ Ð¼Ð°ÑÐµÐ¼Ð°ÑÐ¸ÑÐµÑÐºÐ¸Ð¹ Ð°Ð¿Ð¿Ð°ÑÐ°Ñ Ð¼ÐµÑÐ¾Ð´Ð° ÑÐµÐ·Ð¾Ð»ÑÑÐ¸Ð¹, Ð¿ÑÐ¸Ð²Ð¾Ð´Ð¸ÑÑÑ ÑÐµÐ¾ÑÐµÑÐ¸ÑÐµÑÐºÐ¾Ðµ Ð¾Ð¿Ð¸ÑÐ°Ð½Ð¸Ðµ Ð²ÑÐ±ÑÐ°Ð½Ð½ÑÑ Ð´Ð»Ñ Ð¸ÑÑÐ»ÐµÐ´Ð¾Ð²Ð°Ð½Ð¸Ñ ÑÑÑÐ°ÑÐµÐ³Ð¸Ð¹ Ð¾Ð¿ÑÐ¸Ð¼Ð¸Ð·Ð°ÑÐ¸Ð¸ Ð¸ Ð°Ð»Ð³Ð¾ÑÐ¸ÑÐ¼Ð¾Ð² ÑÐ½Ð¸ÑÐ¸ÐºÐ°ÑÐ¸Ð¸. Ð ÑÑÐµÑÑÐµÐ¹ Ð³Ð»Ð°Ð²Ðµ Ð¿ÑÐ¸Ð²ÐµÐ´ÐµÐ½Ñ Ð¾ÑÐ¾Ð±ÐµÐ½Ð½Ð¾ÑÑÐ¸ Ð¿ÑÐ¾Ð³ÑÐ°Ð¼Ð¼Ð½Ð¾Ð¹ ÑÐµÐ°Ð»Ð¸Ð·Ð°ÑÐ¸Ð¸ ÑÐ°Ð·ÑÐ°Ð±Ð¾ÑÐ°Ð½Ð½Ð¾Ð³Ð¾ Ð¿ÑÐ¸Ð»Ð¾Ð¶ÐµÐ½Ð¸Ñ, Ñ Ð¿Ð¾Ð¼Ð¾ÑÑÑ ÐºÐ¾ÑÐ¾ÑÐ¾Ð³Ð¾ Ð¿ÑÐ¾Ð²Ð¾Ð´Ð¸Ð»ÑÑ Ð°Ð½Ð°Ð»Ð¸Ð·. Ð ÑÐµÑÐ²ÐµÑÑÐ¾Ð¹ Ð³Ð»Ð°Ð²Ðµ Ð²ÑÐ¿Ð¾Ð»Ð½ÐµÐ½Ð¾ ÑÑÐ°Ð²Ð½ÐµÐ½Ð¸Ðµ ÑÑÑÐµÐºÑÐ¸Ð²Ð½Ð¾ÑÑÐ¸ Ð¸ÑÐ¿Ð¾Ð»ÑÐ·Ð¾Ð²Ð°Ð½Ð¸Ñ Ð¸ÑÑÐ»ÐµÐ´ÑÐµÐ¼ÑÑ Ð°Ð»Ð³Ð¾ÑÐ¸ÑÐ¼Ð¾Ð² ÑÐ½Ð¸ÑÐ¸ÐºÐ°ÑÐ¸Ð¸ Ð² ÑÑÑÐ°ÑÐµÐ³Ð¸ÑÑ Ð¾Ð¿ÑÐ¸Ð¼Ð¸Ð·Ð°ÑÐ¸Ð¸ Ð¼ÐµÑÐ¾Ð´Ð° ÑÐµÐ·Ð¾Ð»ÑÑÐ¸Ð¹. ÐÐ° Ð¾ÑÐ½Ð¾Ð²Ð°Ð½Ð¸Ð¸ Ð¿ÑÐ¾Ð²ÐµÐ´ÐµÐ½Ð½Ð¾Ð³Ð¾ Ð¸ÑÑÐ»ÐµÐ´Ð¾Ð²Ð°Ð½Ð¸Ñ Ð½Ð°Ð¸Ð±Ð¾Ð»ÐµÐµ ÑÑÑÐµÐºÑÐ¸Ð²Ð½Ð¾Ð¹ Ð¸Ð· Ð²ÑÐµÑ ÑÐ°ÑÑÐ¼Ð¾ÑÑÐµÐ½Ð½ÑÑ Ð² ÑÐ°Ð±Ð¾ÑÐµ Ð¿ÑÐ¾ÑÐµÐ´ÑÑ ÑÐ½Ð¸ÑÐ¸ÐºÐ°ÑÐ¸Ð¸ Ð¾ÐºÐ°Ð·Ð°Ð»Ð°ÑÑ Ð¿Ð¾Ð»Ð¸Ð½Ð¾Ð¼Ð¸Ð°Ð»ÑÐ½Ð°Ñ Ð¼Ð¾Ð´Ð¸ÑÐ¸ÐºÐ°ÑÐ¸Ñ Ð°Ð»Ð³Ð¾ÑÐ¸ÑÐ¼Ð° Ð Ð¾Ð±Ð¸Ð½ÑÐ¾Ð½Ð°.
description: 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.