Details

Title: Сравнительное исследование эффективности стратегий оптимизации метода резолюций c применением полиномиальной унификации Робинсона: выпускная квалификационная работа магистра: направление 02.04.03 «Математическое обеспечение и администрирование информационных систем» ; образовательная программа 02.04.03_01 «Математическое обеспечение и администрирование корпоративных информационных систем»
Creators: Дедов Алексей Александрович
Scientific adviser: Пак Вадим Геннадьевич
Other creators: Пархоменко Владимир Андреевич
Organization: Санкт-Петербургский политехнический университет Петра Великого. Институт компьютерных наук и технологий
Imprint: Санкт-Петербург, 2021
Collection: Выпускные квалификационные работы; Общая коллекция
Subjects: Вычислительные машины электронные — Программирование - Автоматизация; Математическая физика — Решение задач на вычислительных машинах; метод резолюций; автоматическое доказательство теорем; стратегия оптимизации; алгоритм унификации
UDC: 004.4'24; 51:004
Document type: Master graduation qualification work
File type: PDF
Language: Russian
Level of education: Master
Speciality code (FGOS): 02.04.03
Speciality group (FGOS): 020000 - Компьютерные и информационные науки
Links: Отзыв руководителя; Рецензия; Отчет о проверке на объем и корректность внешних заимствований
DOI: 10.18720/SPBPU/3/2021/vr/vr21-1293
Rights: Доступ по паролю из сети Интернет (чтение, печать, копирование)
Record key: ru\spstu\vkr\14148

Allowed Actions:

Action 'Read' will be available if you login or access site from another network Action 'Download' will be available if you login or access site from another network

Group: Anonymous

Network: Internet

Annotation

Тема выпускной квалификационной работы: «Сравнительное исследование эффективности стратегий оптимизации метода резолюций 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.

Document access rights

Network User group Action
ILC SPbPU Local Network All Read Print Download
External organizations N2 All Read
External organizations N1 All
Internet Authorized users SPbPU Read Print Download
Internet Authorized users (not from SPbPU, N2) Read
Internet Authorized users (not from SPbPU, N1)
-> Internet Anonymous

Usage statistics

stat Access count: 7
Last 30 days: 1
Detailed usage statistics