Автореферат (Автоматический логический вывод в интуиционистских логических исчислениях обратным методом Маслова)

На правах рукописиПавлов Владимир АлександровичАвтоматический логический вывод в интуиционистскихлогических исчислениях обратным методом МасловаСпециальность 05.13.11 —«Математическое и программное обеспечение вычислительных машин,комплексов и компьютерных сетей»Автореферат диссертации на соискание ученой степеникандидата физико-математических наукСанкт-Петербург2017Работа выполнена на кафедре «Компьютерные интеллектуальные технологии» Институтакомпьютерных наук и технологий федерального государственного автономногообразовательного учреждения высшего образования «Санкт-Петербургский политехническийуниверситет Петра Великого»Научный руководитель:Щукин Александр Валентинович,кандидаттехническихнаук,заведующийкафедрой«Компьютерные интеллектуальные технологии» Институтакомпьютерныхнаукитехнологийфедеральногогосударственного автономного образовательного учреждениявысшего образования «Санкт-Петербургский политехническийуниверситет Петра Великого».Официальные оппоненты:Бельтюков Анатолий Петрович,доктор физико-математических наук, профессор, заведующийкафедрой теоретических основ информатики федеральногогосударственного бюджетного образовательного учреждениявысшегообразования«Удмуртскийгосударственныйуниверситет».Соловьев Игорь Павлович,кандидат физико-математических наук, доцент, доцент кафедрыинформатикиматематико-механическогофакультетафедерального государственного бюджетного образовательногоучреждения высшего образования «Санкт-Петербургскийгосударственный университет».Ведущая организация:федеральное государственное бюджетное учреждение наукиСанкт-Петербургское отделение Математического институтаим.

В.А. Стеклова Российской академии наук.Защита состоится «___» _________ 201_ г. в ____ часов на заседании диссертационногосовета Д 212.232.51 на базе Санкт-Петербургского государственного университета по адресу:198504, Санкт-Петербург, Старый Петергоф, Университетский пр., 28, математикомеханический факультет, ауд. 405.С диссертацией можно ознакомиться в Научной библиотеке им. М. Горького СанктПетербургского государственного университета по адресу: 199034, Санкт-Петербург,Университетская наб., 7-9 и на сайте https://disser.spbu.ru/files/disser2/disser/LKfkdgQnht.pdf.Автореферат разослан «___» _________ 201_ г.Ученый секретарьдиссертационного совета Д 212.232.51доктор физико-математических наук, профессорДемьянович Юрий КазимировичОбщая характеристика работыАктуальность темы исследованияДиссертационная работа посвящена применению обратного метода С.

Ю. Маслова дляавтоматизации поиска логического вывода в интуиционистской логике первого порядка.Вопросы автоматизации доказательств изучаются в ведущих научно-исследовательскихинститутах мира. Данная область исследований на стыке математической логики иискусственного интеллекта называется автоматическим логическим выводом (АЛВ).Программные средства для автоматического поиска логического вывода, называемыепрограммами АЛВ («пруверами»), активно применяются в математике, в системахискусственного интеллекта, при решении задач формальной верификации и синтеза ПО 1.Интуиционистские логические исчисления широко используются в математическойлогике и в различных разделах информатики. Одной из наиболее востребованных особенностейэтих исчислений является возможность из доказательства существования некоторого объектаизвлечь способ его построения. В работе под интуиционистской логикой первого порядкапонимается исчисление предикатов А.

Гейтинга и равнообъемные ему исчисления. В отличиеот классического исчисления предикатов, в интуиционистском исчислении неприменимыклассические законы исключенного третьегои снятия двойного отрицания.Программы АЛВ для интуиционистской логики первого порядка находят применение винтерактивных программах АЛВ (для логик высшего порядка), таких как Coq и Nuprl, где онииспользуются в качестве тактик поиска вывода и позволяют частично автоматизироватьрешение сложных задач. Однако эксперименты показывают, что эти тактики пока обладаютнедостаточно высокой результативностью. Поэтому поставленная задача важна для повышениястепени автоматизации интерактивных программ АЛВ, в том числе при их использовании дляверификации и синтеза ПО.Степень разработанности темыСреди методов логического вывода для классической логики первого порядканаибольшеераспространениеиразвитиеполучилметодрезолюций,позволяющийустанавливать выводимость формул, приведенных к сколемовской стандартной форме.

Однакок интуиционистской логике метод резолюций неприменим, так как в ней не все формулы могутбыть приведены к указанному виду эквивалентными преобразованиями.В программах АЛВ для интуиционистской логики обычно используются табличныеметоды логического вывода. Однако существующие программные реализации пока не1Программное обеспечение.3справляются с достаточно сложными задачами, что подтверждается опубликованными в сетиИнтернет результатами их тестирования на библиотеке ILTP. Эта библиотека содержитмножество актуальных задач, включающих задачи из областей формальной верификации,синтеза ПО и различных направлений искусственного интеллекта.В связи с приведенной выше проблемой, особый научный и практический интереспредставляют исследования обратного метода логического вывода, который был предложенС.

Ю. Масловым еще в 1964 году, но начал активно применяться на практике лишь в последнеевремя. Общая схема обратного метода может быть конкретизирована для каждогосеквенциального исчисления, обладающего свойством подформульности (в вывод формулымогут входить лишь ее подформулы). Метод хорошо приспособлен для автоматизации поискавывода в неклассических логиках, использует свойство подформульности для организациипоиска вывода, направленного на целевую формулу. В отличие от ряда табличных методов,обратный метод не требует использования глобальных переменных, выполнения поиска свозвратом и отслеживания циклов.В литературе описано несколько программных реализаций обратного метода дляинтуиционистской логики первого порядка, из которых выделяются программы Gandalf иImogen.

При этом корректность первой программы подвергается сомнению. Вторая программаявляется достаточно эффективной, но ее авторы не используют ряд стратегий поиска вывода,предложенныхвработахС. Ю. Маслова,В. П. Оревкова,Г. Е. Минца,А. Воронкова,А. Дегтярева, Т. Таммета. В то же время стратегии из приведенных работ могут помочьустранить множество избыточных ветвей дерева поиска вывода.Все вышеизложенное раскрывает актуальную потребность ликвидации указанногопробела между теорией и практикой за счет применения существующих результатов из теорииобратного метода при разработке алгоритмов и программ поиска вывода в интуиционистскихисчислениях.

Кроме того, в литературе отсутствуют экспериментальные сравнения стратегий,предложенных разными авторами. Но такое сравнение полезно для построения экономной сточки зрения используемых ресурсов (процессорного времени, оперативной памяти и т. д.)программной реализации обратного метода.Цель и задачи диссертационной работыЦелью работы является построение математического аппарата и алгоритма поискалогического вывода в интуиционистских исчислениях на основе обратного методаС.

Ю. Маслова с последующей разработкой программного обеспечения, позволяющегорасширить спектр решаемых задач в сравнении с существующими программами АЛВ дляинтуиционистской логики.4Для оценки возможности достижения поставленной цели следует разработать программуАЛВ, провести ее тестирование и сравнить с существующими программами АЛВ на задачах избиблиотеки ILTP, руководствуясь признанными мировыми практиками.Для достижения цели были поставлены следующие задачи:1. Выполнить исследование области АЛВ и научных работ по обратному методу.2. Построить интуиционистское исчисление обратного метода, дополнить его стратегиямипоиска вывода для уменьшения размера пространства поиска вывода.3. Сформулировать алгоритм поиска вывода в полученном логическом исчислении.Реализовать алгоритм в виде программы АЛВ с возможностью комбинированияпредложенных стратегий.

В целях повышения гибкости программы предусмотретьинтерактивный режим взаимодействия с пользователем.4. Выполнить экспериментальное сравнение стратегий, выявить оптимальный наборстратегий. Провести тестирование программы и сравнить ее с другими программами назадачах из ILTP, включая задачи из области верификации ПО.Цель и задачи диссертационной работы соответствуют специальности 05.13.11«Математическое и программное обеспечение вычислительных машин, комплексов икомпьютерных сетей», в частности, пунктам 11 и 72 из паспорта этой специальности.Объект и предмет исследованияОбъектом исследования являются методы, алгоритмы и программные средстваавтоматического логического вывода.