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

Артемьев, Андрей Сергеевич. Разработка приложения для решения математических задач методами АДТ [Электронный ресурс]: бакалаврская работа: 02.03.03 / А. С. Артемьев; Санкт-Петербургский политехнический университет Петра Великого, Институт компьютерных наук и технологий ; науч. рук. В. Г. Пак. — Электрон. текстовые дан. (1 файл : 1,08 Мб). — Санкт-Петербург, 2017. — Загл. с титул. экрана. — Свободный доступ из сети Интернет (чтение). — Adobe Acrobat Reader 7.0. — <URL:http://elib.spbstu.ru/dl/2/v17-1732.pdf>. — <URL:http://doi.org/10.18720/SPBPU/2/v17-1732>.

Дата создания записи: 19.04.2017

Тематика: система автоматического доказательства теорем; АДТ; логика предикатов первого порядка

Коллекции: Выпускные квалификационные работы; Общая коллекция

Ссылки: DOI

Разрешенные действия: Прочитать Для чтения документа необходим Flash Player

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

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

Аннотация

Объектом исследования является автоматический логический вывод. Целью данной работы является разработка программы автоматического логического вывода методом резолюций в классической логике предикатов первого порядка, имеющую возможность выбора различных тактик оптимизаций доказательства, с последующим экспериментальным сравнением эффективности данных тактик применительно к усечению дерева пространства поиска. В процессе исследования была рассмотрена классическая логика предикатов первого порядка, её синтаксис и семантика, правила вывода в ней, метод резолюций со стратегиями оптимизации и наиболее успешные системы АДТ (пруверы), их сферы применения и структурные особенности, лежащие внутри них. Была алгоритмизирована общая модель работы прувера для метода резолюций в логике предикатов первого порядка, алгоритмизированы стратегии оптимизации данного метода, разработаны требования к системе и создана рабочая структура программы. Программа автоматического логического вывода со стратегиями оптимизации была реализована на серверной стороне в виде CGI-скриптов на языке Python, создан вэб-интерфейс для взаимодействия с ней. В ходе тестирования и экспериментального сравнения имплементированных в систему стратегий оптимизации и их комбинаций, на разнородных наборах математических задач было выявлено, что наиболее эффективной комбинацией стратегий (с точки зрения усечения дерева поиска и уменьшения времени доказательства) будет Линейная резолюция + Резолюция от цели + Стратегия набора поддержки. Данная комбинация оказалась производительнее Стратегии насыщения уровней в 37 раз, однако она смогла вывести не все утверждения, из чего можно сделать заключение о том, что оптимальным будет параллельное использование быстрой комбинации и более надёжной изолированной стратегии, например, Стратегии набора поддержки.

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

Место доступа Группа пользователей Действие
Локальная сеть ИБК СПбПУ Все Прочитать
-> Интернет Все Прочитать

Статистика использования документа

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