Автореферат (1149225), страница 2
Текст из файла (страница 2)
Предметом исследования являются обоснование иразработка математического и программного обеспечения для решения задачи автоматическогопоиска вывода в интуиционистских логических исчислениях.Методология и методы исследованияВ работе используется признанная методология исследований в области программнойинженерии: идентификация и анализ проблемы, обзор существующей литературы, постановказадачи и выбор подходящих средств ее решения, реализация найденного решения в видепрограммного инструмента, апробация и анализ результатов.Для решения поставленных задач использованы теория и методы математическойлогики, теории доказательств, объектно-ориентированного программирования, планированияинженерных экспериментов.1П.
1 «Модели, методы и алгоритмы проектирования и анализа программ и программных систем, их эквивалентныхпреобразований, верификации и тестирования».2П. 7 «Человеко-машинные интерфейсы...».5Основные положения, выносимые на защиту1. Построено новое интуиционистское исчисление обратного метода для вывода формуллогикипервогопорядка,доказанаегоравнообъемностьисчислениюGHPCА. Г.
Драгалина. Выводы в построенном исчислении могут содержать секвенции болееобщего вида по сравнению с выводами в существующих интуиционистских исчисленияхобратного метода. Предложены стратегии поиска вывода для этого исчисления (включаяновые стратегии для обратного метода), позволяющие уменьшить размер пространствапоиска вывода. Доказана полнота каждой стратегии и любой их комбинации.2. Разработан алгоритм поиска вывода, применимый к разным исчислениям обратногометода. На его основе создана программа АЛВ, позволяющая за счет комбинированияпредложенных в работе стратегий решить новые задачи, которые не могут решитьсуществующие программы АЛВ для интуиционистской логики.3.
Проведено экспериментальное сравнение используемых стратегий по ряду критериев назадачах различной сложности.Научная новизнаНаучная новизна диссертационной работы обусловлена:1. Разработанным математическим аппаратом, включающим новое интуиционистскоеисчисление обратного метода, выводы в котором могут содержать секвенции болееобщего вида по сравнению с выводами в существующих интуиционистских исчисленияхобратного метода, а также адаптированные для этого исчисления и новые стратегиипоиска вывода.2. Сформулированным алгоритмом поиска вывода в полученном исчислении и егореализацией в виде программы АЛВ с возможностью комбинирования стратегий.3. Результатами экспериментов по многокритериальному сравнению всех внедренныхстратегий на актуальных задачах различной сложности.Теоретическая и практическая значимость работыОсновная теоретическая ценность работы заключается в новых результатах, касающихсяисследования свойств интуиционистских исчислений обратного метода и стратегий поискавывода в этих исчислениях.Практическую ценность несут в себе предложенный алгоритм поиска вывода,разработанная на его основе программа АЛВ, результаты проведенных экспериментов, а такжепримеры доказательства теорем обратным методом, приведенные в тексте диссертации.6Достоверность основных положенийДостоверность основных положений диссертационной работы подтверждается: всесторонним анализом существующих научно-исследовательских работ по обратномуметоду и другим методам логического вывода; доказательством равнообъемности построенного исчисления и исчисления GHPC,доказательствами полноты стратегий; проведением исследований и анализом их результатов в соответствии с признаннымимировыми практиками; тестированием программы АЛВ на обширной выборке задач из библиотеки ILTP исравнением с существующими программами.Апробация работыОсновные положения работы докладывались, обсуждались и получили одобрениенаучной общественности на семинарах кафедры системного программирования Математикомеханического факультета СПбГУ, на семинарах «Информатика и компьютерные технологии»в СПИИРАН и «Городской семинар по математической логике» в ПОМИ РАН, а также на 10международных и всероссийских конференциях и семинарах: XXXIX, XL и XLI международные конференции «Неделя науки СПбГПУ»; 4-я международная конференция «Knowledge Engineering and Semantic Web» (2013); XXI и XXII международные семинары «Nonlinear Phenomena in Complex Systems»(NPSC’2014 и NPCS’2015); XVII международная конференция «Foundations & Advances in Nonlinear Science» (2014); международный симпозиум «Mathematics of XXI Century & Natural Science» (2015); XXIII международная научная конференция «Ломоносов-2016»; 11-я международная Ершовская конференция по информатике (PSI–2017).Актуальность исследований и результатов диссертационной работы подтверждаетсяпобедой на конкурсе грантов 2013 года для студентов и аспирантов вузов Санкт-Петербурга.Публикации по теме работыРезультаты, полученные в ходе работы над диссертацией, нашли отражение в 10научных работах, из которых 5 [1-5] содержат основные результаты работы: статьи [1] и [2] опубликованы в издании из перечня российских рецензируемых научныхжурналов, в которых должны быть опубликованы основные результаты диссертаций; работы [3] и [4] опубликованы в зарубежных изданиях, входящих в реферативную базуданных Scopus, т.
е. приравниваемых к изданиям, входящим в вышеуказанный перечень;7 имеется свидетельство о государственной регистрации программы для ЭВМ [5].Статьи [2, 4] и публикации в трудах конференций [3, 7–10] написаны в соавторстве. Вэтих работах В. Г. Паку, А. В. Щукину и Т. Х. Черкасовой принадлежит постановка задач.В. Г. Паку также принадлежит обзор литературы по обратному методу в статье [4]. Остальныерезультаты в указанных работах принадлежат диссертанту.
В частности, соискателюпринадлежат: новое интуиционистское исчисление обратного метода, адаптированные и новыестратегии поиска вывода, формулировки теорем и идеи доказательств, алгоритм поиска выводаи программная реализация, эксперименты с программой, примеры вывода формул.Личный вклад автора. Результаты работы получены соискателем самостоятельно.Структура и объем работыДиссертация состоит из введения, четырех глав, заключения, списка сокращений иусловных обозначений, списка литературы из 162 наименований и четырех приложений.Общий объем работы составляет 223 страницы, включая 64 страницы приложений.Содержание работыВо введении к диссертационной работе обосновывается актуальность поставленнойзадачи, формулируются цели и задачи исследования, научная новизна и практическаязначимость, а также сведения об апробации работы.Первая глава работы содержит обзор предметной области: программы АЛВ и ихприменение, методы поиска вывода для логики предикатов (метод резолюций, табличныеметоды, обратный метод).
Приводится подробный обзор публикаций по обратному методу.Вторая глава посвящена построению нового интуиционистского исчисления обратногометодадля вывода формул логики первого порядка. Аксиомы и правила выводаполученного исчислениязависят от доказываемой формулы .Соглашение. В названии логического исчисления и в дальнейшем изложенииобозначает замкнутую очищенную предикатную формулу, т.
е. формулу без свободныхпеременных, в которой все кванторы связывают разные переменные. Кроме того, формуланедолжна содержать вырожденных кванторов и может содержать только пропозициональныесвязки , , ,и символы кванторов , .Запись видаобозначает множество всех переменных формулы,а—множество всех ее свободных переменных.Пусть— подстановка,авида.Тогда— множество всех переменных, входящих в термы из8,.Записьобозначает подстановку, содержащую те и только те пары. Записьобозначает подстановкуиз , для которых.Понятия подформул и их вхождений определяются стандартным образом. Так, подвхождением подформулыв формулуформулы , совпадающую сбудем понимать фиксированную связную часть. Вхождение подформулы является положительным, если онорасположено в области действия четного числа отрицаний и посылок импликаций.
В противномслучае вхождение является отрицательным. Например, формуласодержит одно (отрицательное) вхождение подформулыи два вхождения подформулы, первое из которых — отрицательное, а второе — положительное.–атом — это вхождение атомарной подформулы в .–секвенция — это секвенция специального вида:где— отрицательныевхожденияподформулположительные вхождения подформул в ;в—;и— подстановкипроизвольных термов вместо переменных (термы могут содержать предметные константы иназываются –формулами и содержательнофункциональные символы); выражения видасоответствуют формулам вида.Часть –секвенции слева от символа выводимости « » называется ее антецедентом, аправая часть — ее сукцедентом.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
