Детальная информация

Название: Сравнительное исследование эффективности стратегий оптимизации метода резолюций c применением полиномиальной унификации Робинсона: выпускная квалификационная работа магистра: направление 02.04.03 «Математическое обеспечение и администрирование информационных систем» ; образовательная программа 02.04.03_01 «Математическое обеспечение и администрирование корпоративных информационных систем»
Авторы: Дедов Алексей Александрович
Научный руководитель: Пак Вадим Геннадьевич
Другие авторы: Пархоменко Владимир Андреевич
Организация: Санкт-Петербургский политехнический университет Петра Великого. Институт компьютерных наук и технологий
Выходные сведения: Санкт-Петербург, 2021
Коллекция: Выпускные квалификационные работы; Общая коллекция
Тематика: Вычислительные машины электронные — Программирование - Автоматизация; Математическая физика — Решение задач на вычислительных машинах; метод резолюций; автоматическое доказательство теорем; стратегия оптимизации; алгоритм унификации
УДК: 004.4'24; 51:004
Тип документа: Выпускная квалификационная работа магистра
Тип файла: PDF
Язык: Русский
Уровень высшего образования: Магистратура
Код специальности ФГОС: 02.04.03
Группа специальностей ФГОС: 020000 - Компьютерные и информационные науки
Ссылки: Отзыв руководителя; Рецензия; Отчет о проверке на объем и корректность внешних заимствований
DOI: 10.18720/SPBPU/3/2021/vr/vr21-1293
Права доступа: Доступ по паролю из сети Интернет (чтение, печать, копирование)
Ключ записи: ru\spstu\vkr\14148

Разрешенные действия:

Действие 'Прочитать' будет доступно, если вы выполните вход в систему или будете работать с сайтом на компьютере в другой сети Действие 'Загрузить' будет доступно, если вы выполните вход в систему или будете работать с сайтом на компьютере в другой сети

Группа: Анонимные пользователи

Сеть: Интернет

Аннотация

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

Права на использование объекта хранения

Место доступа Группа пользователей Действие
Локальная сеть ИБК СПбПУ Все Прочитать Печать Загрузить
Внешние организации №2 Все Прочитать
Внешние организации №1 Все
Интернет Авторизованные пользователи СПбПУ Прочитать Печать Загрузить
Интернет Авторизованные пользователи (не СПбПУ, №2) Прочитать
Интернет Авторизованные пользователи (не СПбПУ, №1)
-> Интернет Анонимные пользователи

Статистика использования

stat Количество обращений: 7
За последние 30 дней: 0
Подробная статистика