Table | Card | RUSMARC | |
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 |
Annotation
Объектом исследования является автоматический логический вывод. Целью данной работы является разработка программы автоматического логического вывода методом резолюций в классической логике предикатов первого порядка, имеющую возможность выбора различных тактик оптимизаций доказательства, с последующим экспериментальным сравнением эффективности данных тактик применительно к усечению дерева пространства поиска. В процессе исследования была рассмотрена классическая логика предикатов первого порядка, её синтаксис и семантика, правила вывода в ней, метод резолюций со стратегиями оптимизации и наиболее успешные системы АДТ (пруверы), их сферы применения и структурные особенности, лежащие внутри них. Была алгоритмизирована общая модель работы прувера для метода резолюций в логике предикатов первого порядка, алгоритмизированы стратегии оптимизации данного метода, разработаны требования к системе и создана рабочая структура программы. Программа автоматического логического вывода со стратегиями оптимизации была реализована на серверной стороне в виде CGI-скриптов на языке Python, создан вэб-интерфейс для взаимодействия с ней. В ходе тестирования и экспериментального сравнения имплементированных в систему стратегий оптимизации и их комбинаций, на разнородных наборах математических задач было выявлено, что наиболее эффективной комбинацией стратегий (с точки зрения усечения дерева поиска и уменьшения времени доказательства) будет Линейная резолюция + Резолюция от цели + Стратегия набора поддержки. Данная комбинация оказалась производительнее Стратегии насыщения уровней в 37 раз, однако она смогла вывести не все утверждения, из чего можно сделать заключение о том, что оптимальным будет параллельное использование быстрой комбинации и более надёжной изолированной стратегии, например, Стратегии набора поддержки.
Document access rights
Network | User group | Action | ||||
---|---|---|---|---|---|---|
ILC SPbPU Local Network | All | |||||
Internet | Authorized users SPbPU | |||||
Internet | Anonymous |
Usage statistics
Access count: 113
Last 30 days: 0 Detailed usage statistics |