Диссертация (1149226), страница 2
Текст из файла (страница 2)
Эта библиотека содержит множествоактуальных задач, включающих задачи из областей формальной верификации,синтеза ПО и различных направлений искусственного интеллекта [121].В связи с приведенной выше проблемой, особый научный и практическийинтерес представляют исследования обратного метода логического вывода,который был предложен С. Ю. Масловым еще в 1964 году [21], но начал активноприменяться на практике лишь в последнее время.
Общая схема обратного метода[22] может быть конкретизирована для каждого секвенциального исчисления,обладающего свойством подформульности (в вывод формулы могут входитьлишь ее подформулы). Метод хорошо приспособлен для автоматизации поискавывода в неклассических логиках, использует свойство подформульности дляорганизации поиска вывода, направленного на целевую формулу.
В отличие от6ряда табличных методов, обратный метод не требует использования глобальныхпеременных, выполнения поиска с возвратом и отслеживания циклов.В литературе описано несколько программных реализаций обратногометода для интуиционистской логики первого порядка, из которых выделяютсяпрограммы Gandalf [139] и Imogen [106].
При этом корректность первойреализации подвергается сомнению [144]. Вторая реализация является достаточноэффективной [106], но ее авторы не используют ряд стратегий поиска вывода,предложенных в работах С. Ю. Маслова [20], В. П. Оревкова [38], Г. Е. Минца[109], А. Воронкова и А. Дегтярева [157, 68], Т.
Таммета [139]. В то же времястратегии из приведенных работ могут помочь устранить множество избыточныхветвей дерева поиска вывода.Все вышеизложенное раскрывает актуальную потребность ликвидацииуказанногопробеламеждутеориейипрактикойзасчетприменениясуществующих результатов из теории обратного метода при разработкеалгоритмов и программ поиска вывода в интуиционистских исчислениях. Крометого, в литературе отсутствуют экспериментальные сравнения стратегий,предложенных разными авторами.
Но такое сравнение полезно для построенияэкономной с точки зрения используемых ресурсов (процессорного времени,оперативной памяти и т. д.) программной реализации обратного метода.Цель и задачи диссертационной работыЦелью работы является построение математического аппарата и алгоритмапоиска логического вывода в интуиционистских исчислениях на основе обратногометода С. Ю. Маслова, с последующей реализацией программного обеспечения,позволяющего расширить спектр решаемых задач в сравнении с существующимипрограммами АЛВ для интуиционистской логики.Дляразработатьоценкивозможностипрограмму АЛВ,существующимипрограммамидостиженияпровестиАЛВнаеепоставленнойтестированиезадачахизцелиисравнитьбиблиотекируководствуясь признанными мировыми практиками.Для достижения цели были поставлены следующие задачи:следуетсILTP,71.
Выполнить исследование современного состояния области АЛВ и научныхработ по обратному методу.2. Выбрать подходящее интуиционистское исчисление обратного метода4,дополнить его стратегиями поиска вывода для уменьшения размерапространства поиска вывода.3. Сформулировать алгоритм поиска вывода в полученном логическомисчислении. Реализовать алгоритм в виде программы АЛВ с возможностьюкомбинирования предложенных стратегий. В целях повышения гибкостипрограммыпредусмотретьинтерактивныйрежимвзаимодействияспользователем.4. Выполнить экспериментальное сравнение стратегий на задачах разнойсложности, выявить оптимальный набор стратегий.
Провести тестированиепрограммы и сравнить ее с другими программами на задачах из ILTP,включая задачи из области верификации ПО.Цельиспециальностизадачидиссертационной05.13.11работы«Математическоеисоответствуютпрограммноеформулеобеспечениевычислительных машин, комплексов и компьютерных сетей»5 и областямисследования из паспорта этой специальности, в частности, пунктам 16 и 77.Объект и предмет исследованияОбъектом исследования являются методы, алгоритмы и программныесредстваавтоматическогологическоговывода.Предметомисследованияявляются разработка, обоснование и реализация математического и программногообеспечениядлярешениязадачиавтоматическогопоискавыводавинтуиционистских логических исчислениях.4Здесь и далее используется аналог англоязычного термина «inverse method calculus» из работы [68].5В паспорте указанная специальность определена как «специальность, включающая задачи развитиятеории программирования, создания и сопровождения программных средств различного назначения».6П.
1 «Модели, методы и алгоритмы проектирования и анализа программ и программных систем, ихэквивалентных преобразований, верификации и тестирования».7П. 7 «Человеко-машинные интерфейсы...».8Методология и методы исследованияВ работе используется признанная методология исследований в областипрограммнойинженерии:идентификацияианализпроблемы,обзорсуществующей литературы, постановка задачи и выбор подходящих средств еерешения, реализация найденного решения в виде программного инструмента,апробация и анализ результатов.Для решения поставленных задач использованы теория и методыматематической логики, теории доказательств, объектно-ориентированногопрограммирования, планирования инженерных экспериментов.Основные положения, выносимые на защиту1. Построено новое интуиционистское исчисление обратного метода длявывода формул логики первого порядка, доказана его равнообъемностьисчислению GHPC А.
Г. Драгалина [10]. Выводы в построенном исчислениимогут содержать секвенции более общего вида по сравнению с выводами всуществующихинтуиционистскихисчисленияхобратногометода.Разработаны стратегии поиска вывода для этого исчисления (включая новыестратегии для обратного метода), позволяющие уменьшить размерпространства поиска вывода. Доказана полнота каждой стратегии и любойих комбинации.2. Разработан алгоритм поиска вывода, применимый к разным исчислениямобратного метода. На его основе реализована программа АЛВ, позволяющаяза счет комбинирования предложенных в работе стратегий решить новыезадачи, которые не могут решить существующие программы АЛВ дляинтуиционистской логики.3. Проведено экспериментальное сравнение используемых стратегий по рядукритериев на задачах различной сложности.Научная новизнаНаучная новизна диссертационной работы обусловлена:91.
Разработаннымматематическимаппаратом,включающимновоеинтуиционистское исчисление обратного метода, выводы в котором могутсодержать секвенции более общего вида по сравнению с выводами всуществующих интуиционистских исчислениях обратного метода, а такжеадаптированные для этого исчисления и новые стратегии поиска вывода.2. Сформулированным алгоритмом поиска вывода в полученном исчислении иего реализацией в виде программы АЛВ с возможностью комбинированияпредложенных стратегий.3.
Результатами экспериментов по многокритериальному сравнению всехвнедренных стратегий на актуальных задачах различной сложности.Теоретическая и практическая значимость работыОсновная теоретическая ценность работы заключается в новых результатах,касающихся исследования свойств интуиционистских исчислений обратногометода и стратегий поиска вывода в этих исчислениях.Практическую ценность несут в себе предложенный алгоритм поискавывода, разработанная на его основе программа АЛВ, результаты проведенныхэкспериментов, а также примеры доказательства теорем обратным методом,приведенные в тексте диссертации.Достоверность основных положенийДостоверностьосновныхположенийдиссертационнойработыподтверждается: всесторонним анализом существующих научно-исследовательских работ пообратному методу и другим методам логического вывода; доказательством равнообъемности построенного исчисления и исчисленияGHPC, доказательствами полноты стратегий; проведением исследований и анализом их результатов в соответствии спризнанными мировыми практиками; тестированием программы АЛВ на обширной выборке задач из библиотекиILTP и сравнением с существующими программами.10Апробация работыОсновные положения работы докладывались, обсуждались и получилиодобрениенаучнойобщественностинасеминарахкафедрыСистемногопрограммирования Математико-механического факультета СПбГУ, на семинарах«Информатика и компьютерные технологии» в СПИИРАН и «Городской семинарпо математической логике» в ПОМИ РАН, а также на 10 международных ивсероссийских конференциях и семинарах: XXXIX, XL и XLI международные конференции «Неделя науки СПбГПУ»; 4-я международная конференция «Knowledge Engineering and SemanticWeb» (KESW’2013); XXI и XXII международные семинары «Nonlinear Phenomena in ComplexSystems» (NPSC’2014 и NPCS’2015); XVII международная конференция «Foundations & Advances in NonlinearScience» (FANS’2014); международный симпозиум «Mathematics of XXI Century & Natural Science»(2015); XXIII международная научная конференция студентов, аспирантов имолодых ученых «Ломоносов-2016»; 11-я международная Ершовская конференция по информатике (PSI–2017).Актуальность исследований и результатов диссертационной работыподтверждается победой на конкурсе грантов 2013 года для студентов иаспирантов вузов Санкт-Петербурга.Публикации по теме работыРезультаты, полученные в ходе работы над диссертацией, нашли отражениев 10 научных работах, из которых 5 [114, 116, 44, 48, 45] содержат основныерезультаты работы: статьи [45] и [44] опубликованы в издании из перечня российскихрецензируемых научных журналов, в которых должны быть опубликованыосновные результаты диссертаций;11 работы [116] и [114] опубликованы в зарубежных изданиях, входящих вреферативную базу данных Scopus, т.
е. приравниваемых к изданиям,входящим в перечень; имеется свидетельство о государственной регистрации программы дляЭВМ [48].Статьи [116, 44] и публикации в трудах конференций [41, 43, 42, 114, 115]написанывсоавторстве.ВэтихработахВ. Г. Паку,А. В. ЩукинуиТ. Х. Черкасовой принадлежит постановка задач. В. Г. Паку также принадлежитисторический обзор литературы по обратному методу в статье [116]. Остальныерезультаты в указанных работах принадлежат диссертанту. В частности,соискателю принадлежат: новое интуиционистское исчисление обратного метода,адаптированные и новые стратегии поиска вывода, формулировки теорем и идеидоказательств, алгоритм поиска вывода и программная реализация, экспериментыс программой, примеры вывода формул обратным методом.Личный вклад автора.
Результаты диссертационной работы полученысоискателем самостоятельно.Структура и объем работыДиссертация состоит из введения, четырех глав, заключения, спискасокращений и условных обозначений, списка литературы из 162 наименований ичетырех приложений. Общий объем работы составляет 223 страницы, включая 64страницы приложений.Краткий план последующих глав диссертацииВ главе 1 приводится обзор предметной области: интуиционизм иинтуиционистская логика, программы АЛВ и их применение, методы АЛВ длялогики первого порядка.Вглаве2рассматриваетсяпостроениеновогоинтуиционистскогоисчисления обратного метода, которое ближе к классическим исчислениям, чемсуществующие интуиционистские исчисления обратного метода.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
