Details

Title: Разработка приложения для решения математических задач методами АДТ: бакалаврская работа: 02.03.03
Creators: Артемьев Андрей Сергеевич
Scientific adviser: Пак Вадим Геннадьевич
Organization: Санкт-Петербургский политехнический университет Петра Великого. Институт компьютерных наук и технологий
Imprint: Санкт-Петербург, 2017
Collection: Выпускные квалификационные работы; Общая коллекция
Subjects: система автоматического доказательства теорем; АДТ; логика предикатов первого порядка
Document type: Bachelor graduation qualification work
File type: PDF
Language: Russian
Speciality code (FGOS): 02.03.03
Speciality group (FGOS): 020000 - Компьютерные и информационные науки
Links: http://doi.org/10.18720/SPBPU/2/v17-1732
Rights: Свободный доступ из сети Интернет (чтение)

Allowed Actions: Read You need Flash Player to read document

Group: Anonymous

Network: FL SPbPU Local Network

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: 81
Last 30 days: 7
Detailed usage statistics