Автореферат (1149225), страница 4
Текст из файла (страница 4)
В число этих задач входят 88 задач, которыене были решены ни одной из шести программ, официальные результаты которых представленына сайте ILTP: JProver, ft-C, ft-Prolog, ileanSeP, ileanTAP, ileanCoP (1.0). По сравнению со всемисемью программами, включая Imogen, программа WhaleProver решила 16 новых задач с14известным статусом. Кроме того, программа позволяет решить ряд задач значительно быстреедругих программ. Подробные результаты сравнения приведены в тексте диссертации.В программе предусмотрен интерактивный режим, позволяющий решить некоторыезадачи, которые программа WhaleProver и другие программы не могут решить вавтоматическом режиме.
В диссертации рассматривается пример решения задачи из областиверификации ПО.В заключении сформулированы основные выводы, итоги выполненного исследования,рекомендации, перспективы дальнейшей разработки темы.В приложения вынесены доказательства промежуточных утверждений, результатыпрограммы на задачах из ILTP и сведения о задачах, использованных при сравнении стратегий.ЗаключениеИтоги диссертационной работы таковы:1.
Выполнено исследование современного состояния предметной области.2. Построено новое интуиционистское исчисление обратного методадля выводаформул логики первого порядка, доказана его равнообъемность исчислению GHPCА. Г. Драгалина. Исчисление дополнено стратегиями поиска вывода, включая новыестратегии. Доказана полнота любой комбинации предложенных стратегий.3. Предложен алгоритм поиска вывода, применимый к разным исчислениям обратногометода. На его основе разработана программа АЛВ, за счет комбинирования стратегийпозволяющая решить новые задачи, которые не могут решить существующиепрограммы.
В программе предусмотрен интерактивный режим, дающий возможностьрешать больше сложных задач, в том числе из области верификации ПО.4. Проведено тестирование программы на задачах из библиотеки ILTP, полученырезультаты экспериментального сравнения стратегий по ряду критериев.Сформулированы следующие рекомендации по применению полученных результатов:1. Разработанную программу рекомендуется применять для решения математических итехнических задач, формализуемых на языке логики первого порядка.2. Результаты экспериментального сравнения стратегий желательно учитывать приразработке программ АЛВ на основе обратного метода.Определены перспективы дальнейшей разработки темы:1.
Использование разработанной программы в качестве экспериментальной платформы дляиспытания исчислений обратного метода и стратегий поиска вывода.2. Использование программы в рамках учебного курса «Математическая логика».3. Интеграция разработанной программы в интерактивные программы АЛВ (Coq, Nuprl).15Список опубликованных работ по теме диссертацииВ изданиях из перечня российских рецензируемых научных журналов, в которыхдолжны быть опубликованы основные научные результаты диссертаций насоискание ученых степеней доктора и кандидата наук1. Павлов, В. Эффективная программная реализация обратного метода Маслова дляинтуиционистской логики // Научно-технические ведомости СПбГПУ. Информатика.Телекоммуникации.
Управление. — 2017. — № 1. — С. 49–62.2. Павлов, В. Экспериментальная программа для доказательства теорем интуиционистскойлогики обратным методом Маслова / В. Павлов, В. Пак // Научно-технические ведомостиСПбГПУ. Информатика. Телекоммуникации. Управление. — 2015. — № 6. — С. 70–80.В изданиях, индексируемых в реферативных базах Scopus и Web Of Science3. Pavlov, V. Exploring Automated Reasoning in First-Order Logic: Tools, Techniques andApplication Areas / V. Pavlov, A. Schukin, T.
Cherkasova // 4th International ConferenceKnowledge Engineering and the Semantic Web (KESW 2013). Communications in Computerand Information Science (CCIS). — Springer Berlin Heidelberg, 2013. — Vol. 394. — P. 102–116.4. Pavlov, V. The Inverse Method Application for Non-Classical Logics / V.
Pavlov, V. Pak //Nonlinear Phenomena in Complex Systems. — 2015. — 18 (2). — P. 181–190.Свидетельства о регистрации программных продуктов5. Свидетельство № 2016615547. Программа для автоматического доказательства теорем винтуиционистских логических исчислениях обратным методом Маслова «WhaleProver»(WhaleProver) / автор и правообладатель Павлов В. А. — № 2016612689 ; заявл.28.03.2016 ; зарегистр. 26.05.2016.В других изданиях6. Павлов, В. А.
Алгоритм и программное средство автоматического логического выводаформул интуиционистской логики // Ломоносов-2016: Материалы XXIII Международнойнаучнойконференциистудентов,аспирантовимолодыхученых:секция«Вычислительная математика и кибернетика». — М. : Издательский отдел факультетаВМК МГУ, 2016. — C. 44–47.7. Pavlov, V. The Inverse Method and First-Order Logic Theorem Proving / V. Pavlov, V. Pak //Nonlinear Dynamics and Applications. — 2014.
— Vol. 20. — P. 127–135.168. Павлов, В. А. Сравнение эффективности методов автоматического доказательстватеорем / В. А. Павлов, В. Г. Пак // Материалы XXXIX международной научнопрактической конференции «Неделя науки СПбГПУ». — СПб. : Изд-во СПбГПУ,2011. — С. 62–65.9. Павлов, В. А. Сравнительное исследование методов автоматического логическоговывода для логики предикатов / В. А. Павлов, В. Г.
Пак // XL Неделя науки СПбГПУ:материалы международной научно-практической конференции. Часть XVIII. — СПб. :Изд-во Политехн. ун-та, 2011. — С. 10–12.10. Павлов, В. А. Сравнение эффективности методов автоматического доказательстватеорем / В. А. Павлов, В. Г. Пак // XXXIX Неделя науки СПбГПУ. Материалымеждународной научно-практической конференции. Часть XVIII. Факультет управленияи информационных технологий. — СПб.
: Изд-во СПбГПУ, 2010. — С. 13–15._____________________________________________________________________________Подписано в печать 10..2017. Формат 60х84/16. Печать цифровая.Усл. печ. л. 1,0. Тираж 100. Заказ 15b._____________________________________________________________________________Отпечатано с готового оригинал-макета, предоставленного автором,в Издательско-полиграфическом центреПолитехнического университета.195251, Санкт-Петербург, Политехническая ул., 29.Тел.: (812) 552-77-17; 550-40-14.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
