Details
Title | Разработка приложения для решения математических задач методами АДТ: бакалаврская работа: 02.03.03 |
---|---|
Creators | Артемьев Андрей Сергеевич |
Scientific adviser | Пак Вадим Геннадьевич |
Organization | Санкт-Петербургский политехнический университет Петра Великого. Институт компьютерных наук и технологий |
Imprint | Санкт-Петербург, 2017 |
Collection | Выпускные квалификационные работы ; Общая коллекция |
Subjects | система автоматического доказательства теорем ; АДТ ; логика предикатов первого порядка |
Document type | Bachelor graduation qualification work |
File type | |
Language | Russian |
Level of education | Bachelor |
Speciality code (FGOS) | 02.03.03 |
Speciality group (FGOS) | 020000 - Компьютерные и информационные науки |
DOI | 10.18720/SPBPU/2/v17-1732 |
Rights | Доступ по паролю из сети Интернет (чтение, печать, копирование) |
Record key | RU\SPSTU\edoc\38632 |
Record create date | 4/19/2017 |
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 |
Объектом исследования является автоматический логический вывод. Целью данной работы является разработка программы автоматического логического вывода методом резолюций в классической логике предикатов первого порядка, имеющую возможность выбора различных тактик оптимизаций доказательства, с последующим экспериментальным сравнением эффективности данных тактик применительно к усечению дерева пространства поиска. В процессе исследования была рассмотрена классическая логика предикатов первого порядка, её синтаксис и семантика, правила вывода в ней, метод резолюций со стратегиями оптимизации и наиболее успешные системы АДТ (пруверы), их сферы применения и структурные особенности, лежащие внутри них. Была алгоритмизирована общая модель работы прувера для метода резолюций в логике предикатов первого порядка, алгоритмизированы стратегии оптимизации данного метода, разработаны требования к системе и создана рабочая структура программы. Программа автоматического логического вывода со стратегиями оптимизации была реализована на серверной стороне в виде CGI-скриптов на языке Python, создан вэб-интерфейс для взаимодействия с ней. В ходе тестирования и экспериментального сравнения имплементированных в систему стратегий оптимизации и их комбинаций, на разнородных наборах математических задач было выявлено, что наиболее эффективной комбинацией стратегий (с точки зрения усечения дерева поиска и уменьшения времени доказательства) будет Линейная резолюция + Резолюция от цели + Стратегия набора поддержки. Данная комбинация оказалась производительнее Стратегии насыщения уровней в 37 раз, однако она смогла вывести не все утверждения, из чего можно сделать заключение о том, что оптимальным будет параллельное использование быстрой комбинации и более надёжной изолированной стратегии, например, Стратегии набора поддержки.
Network | User group | Action |
---|---|---|
ILC SPbPU Local Network | All |
|
Internet | Authorized users SPbPU |
|
Internet | Anonymous |
|
Access count: 113
Last 30 days: 0