Details

Артемьев, Андрей Сергеевич. Разработка приложения для решения математических задач методами АДТ [Электронный ресурс]: бакалаврская работа: 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>.

Record create date: 4/19/2017

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

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

Links: DOI

Allowed Actions: Read You need Flash Player to read document

Group: Anonymous

Network: Internet

Annotation

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

Document access rights

Network User group Action
FL SPbPU Local Network All Read
-> Internet All Read

Document usage statistics

stat Document access count: 73
Last 30 days: 0
Detailed usage statistics