Диссертация (1149226), страница 24
Текст из файла (страница 24)
Построено новое интуиционистское исчисление обратного методадлявывода формул логики первого порядка, доказана его равнообъемностьисчислению GHPC А. Г. Драгалина. Полученное исчисление ближе кклассическим исчислениям, выводы в этом исчислении могут содержатьсеквенции более общего вида по сравнению с выводами в исчислениииз работы [68] и в других существующих интуиционистских исчисленияхобратного метода. Для исчисленияадаптированы стратегии поискавывода, существующие для других исчислений обратного метода, а такжепредложены новые стратегии. Доказана полнота любой комбинациирассмотренных стратегий.3. Предложеналгоритмпоискавыводавразработанномлогическомисчислении, применимый также к другим исчислениям обратного метода.На основе этого алгоритма разработана программа АЛВ, за счеткомбинирования стратегий позволяющая решить новые задачи, которые немогут решить существующие программы.
В программе предусмотренинтерактивный режим, дающий возможность решать больше сложных142задач, в том числе из области верификации ПО. Полученные результатыподтверждают, что программная реализация обратного метода может бытьне менее эффективной, чем реализации табличных методов.4.
Проведено тестирование программы на задачах из библиотеки ILTP,полученырезультатыэкспериментальногосравненияиспользуемыхстратегий по ряду критериев.Таким образом, в работе решены все поставленные задачи и достигнутапервоначальная цель исследования.Можнопредложитьследующиерекомендациипоиспользованиюполученных результатов и научных выводов:1.
Разработанную программу WhaleProver рекомендуется применять длярешения математических и технических задач, формализуемых на языкелогики первого порядка.2. Результаты экспериментального сравнения стратегий желательно учитыватьпри разработке программ АЛВ на основе обратного метода.3. Идеидоказательствполнотыстратегийможноиспользоватьприобосновании стратегий для других исчислений обратного метода.4. Приведенные в диссертации примеры доказательств обратным методоммогут использоваться при изучении этого метода для большей наглядности.В качестве перспектив дальнейшей разработки темы можно отметить:1.
Продолжение исследований по разработке эффективных стратегий дляобратного метода, в том числе обобщение предложенных стратегий.2. Использование разработанной программы в качестве экспериментальнойплатформы для испытания исчислений обратного метода и стратегийпоиска вывода, а также для практического изучения их свойств.3. Использование программы в качестве наглядного пособия в рамкахучебного курса «Математическая логика».4. Интеграция разработанной программы в существующие интерактивныепрограммы АЛВ (Coq, Nuprl).143СПИСОК СОКРАЩЕНИЙ И УСЛОВНЫХ ОБОЗНАЧЕНИЙАЛВАвтоматический логический выводАДТАвтоматическое доказательство теорем (в работе используетсякак синоним АЛВ)КНФКонъюнктивная нормальная формаОЗУОперативное запоминающее устройствоОСОперационная системаПОПрограммное обеспечениеЭксп.Эксперимент144СПИСОК ИСПОЛЬЗОВАННОЙ ЛИТЕРАТУРЫ1.
Бет, Э. В. Метод семантических таблиц // Математическая теориялогического вывода. — М. : Наука, 1967. — С. 191–199.2. Бурлуцкий, В. В.Реализацияобратногометодаустановлениявыводимости для модальной логики КТ [Текст] : дис. … канд. физ.-мат. наук :05.13.01 Системный анализ, управление и обработка информации (по отраслям).— 2001. — 103 с.3. Гамма, Э.Приемыобъектно-ориентированногопроектирования.Паттерны проектирования / Э. Гамма [и др.] ; пер. с англ.
— СПб. : Питер, 2001.— 368 с.4. Гейтинг, А. Интуиционизм / А. Гейтинг ; пер. с англ. Б. А. Янкоба ; подред. и с коммент. А. А. Маркова. — М. : Мир, 1965. — 202 с.5. Генцен, Г. Исследования логических выводов // Математическая теориялогического вывода. — М. : Наука, 1967. — С. 9–76.6. Давыдов, Г.
В. Машинный алгорифм установления выводимости наоснове обратного метода / Г. В. Давыдов [и др.] // Зап. научн. сем. ЛОМИ. —1969. — Т. 16. — С. 8–19.7. Давыдов, Г. В. Синтез метода резолюций с обратным методом // Зап.научн. сем. ЛОМИ. — 1971. — Т. 20. — С. 24–35.8. Доценко, В. А.
Особенности применения конструктивного алгоритмаобратного метода для секвенциального исчисления предикатов // Искусственныйинтеллект. — 2008. — № 3. — С. 655–662.9. Драгалин, А. Г. Конструктивная теория доказательств и нестандартныйанализ. — М. : Едиториал УРСС, 2003. — 544 с.10. Драгалин, А. Г. Математический интуиционизм. Введение в теориюдоказательств. — М. : Наука, 1979. — 256 с.11.
Кангер, С. Упрощенный метод доказательства для элементарной логики// Математическая теория логического вывода. — М. : Наука, 1967. — С. 200–207.12. Катречко, С. Л. Обратный метод С. Ю. Маслова // Логика и компьютер.— М. : Наука, 1995. — № 2. — С. 62–75.14513. Клини, С. К. Введение в метаматематику / С.
К. Клини ; пер. с англ.А. С. Есенина-Вольпина ; под ред. В. А. Успенского. — М. : Изд-во иностр. лит.,1957. — 527 с.14. Клини, С. К. Математическая логика / С. К. Клини ; пер. с англ. — М. :Мир, 1973. — 480 с.15. Клини, С. К. Основания интуиционистской математики / С. К. Клини,Р. Ю. Весли ; пер. с англ. Ф. А. Кабакова и Б. А. Кушнера. — M. : Наука, 1978. —271 с.16. Клини, С. К.
Перестановочность применений правил в генценовскихисчислениях LK и LJ // Математическая теория логического вывода. — М. :Наука, 1967. — С. 208–236.17. Колмогоров, А. Н. О принципе tertium non datur // Матем. сб. — 1925.— Т. 32. — № 4. — С. 646–667.18. Ларионов, Д. С. Обратный метод установления выводимости дляавтоэпистемической логики и его применение в экспертных системах : дис. …канд. техн. наук : 05.13.01 Системный анализ, управление и обработкаинформации (по отраслям). — 2005. — 148 с.19. Марков, А.
А. О конструктивной математике // Тр. МИАН СССР. —М. : Изд-во АН СССР, 1962. — Т. 67. — С. 8–14.20. Маслов, С. Ю. Обратный метод и тактики установления выводимостидля исчисления с функциональными знаками // Тр. МИАН СССР. — 1972. —Т. 121. — С. 14–56.21. Маслов, С.
Ю.Обратныйметодустановлениявыводимостивклассическом исчислении предикатов // ДАН СССР. — 1964. — Т. 159. — № 1. —С. 17–20.22. Маслов, С. Ю. Обратный метод установления выводимости длялогических исчислений // Тр. МИАН СССР. — 1968. — Т. 98. — С. 26–87.23. Маслов, С. Ю. Обратный метод установления выводимости длянепредваренных формул исчисления предикатов // ДАН СССР. — 1967. — Т. 172.— № 1. — С.
22–25.14624. Маслов, С. Ю. О поиске вывода в исчислениях общего типа // Зап.научн. сем. ЛОМИ. — 1972. — Т. 32. — С. 59–65.25. Маслов, С. Ю.Применениеобратногометодаустановлениявыводимости к теории разрешимых фрагментов классического исчисленияпредикатов // ДАН СССР. — 1966. — Т. 171. — № 6. — С. 1282–1285.26. Маслов, С. Ю. Разрешимые классы, сводящиеся к однокванторномуклассу / С. Ю. Маслов, В. П. Оревков // Тр. МИАН СССР. — 1972. — Т. 121. — С.57–66.27.
Маслов, С. Ю. Распространение обратного метода на исчисление сравенством // Зап. научн. сем. ЛОМИ. — 1971. — Т. 20. — С. 80–96.28. Маслов, С. Ю. Связь между тактиками обратного метода и методарезолюций // Зап. научн. сем. ЛОМИ. — 1969.— Т. 16. — С. 137–146.29. Маслов, С. Ю. Тактики поиска вывода, основанные на унификациипорядка членов в благоприятном наборе // Зап.
научн. сем. ЛОМИ. — 1969. —Т. 16. — С. 126–136.30. Маслов, С. Ю. Теория дедуктивных систем и ее применения. — М. :Радио и связь, 1986. — 136 с.31. Маслов, С. Ю.Теорияпоискавыводаиобратныйметод(вдополнении A) / С. Ю. Маслов, Г. Е. Минц // Математическая логика иавтоматическое доказательство теорем.
— М. : Наука, 1983. — С. 291–314.32. Мендельсон, Э. Введение в математическую логику / Э. Мендельсон ;пер. с англ. Ф. А. Кабакова ; под ред. С. И. Адяна. — М. : Наука, 1971. — 320 с.33. Минц, Г. Е. Резолютивные исчисления для неклассических логик // 9-йСоветский Кибернетический симпозиум. — М. : ВИНИТИ, 1981. — Т. 2. — С. 34–36.34.
Минц, Г. Е. Теорема Эрбрана (приложение) // Математическая теориялогического вывода. — М. : Наука, 1967. — С. 311–350.35. Оревков, В. П. Верхние оценки удлинения выводов при устранениисечений // Зап. научн. сем. ЛОМИ. — 1984 — Т. 137. — С. 87–98.14736.
Оревков, В. П. Два неразрешимых класса формул классическогоисчисления предикатов // Зап. научн. сем. ЛОМИ. — 1968. — Т. 8. — С. 202–210.37. Оревков, В. П. Новый разрешимый хорновский фрагмент исчисленияпредикатов // Зап. научн. сем. ПОМИ. — 2004. — Т. 316. — С. 147–162.38. Оревков, В. П. Обратный метод поиска вывода для скулемовскихпредваренных формул исчисления предикатов (приложение 4) // Логическоепрограммирование и Visual Prolog. — СПб. : БХВ-Петербург, 2003. — С. 952–965.39. Оревков, В. П. О гливенковских классах секвенций // Тр. МИАН СССР.— 1968. — Т.
98. — С. 131–154.40. Павлов, В. А. Алгоритм и программное средство автоматическогологического вывода формул интуиционистской логики // Ломоносов-2016:Материалы XXIII Международной научной конференции студентов, аспирантов имолодых ученых: секция «Вычислительная математика и кибернетика». — М. :Издательский отдел факультета ВМК МГУ, 2016. — C. 44–47.41.
Павлов, В. А. Сравнение эффективности методов автоматическогодоказательства теорем / В. А. Павлов, В. Г. Пак // XXXIX Неделя науки СПбГПУ.Материалы международной научно-практической конференции. Часть XVIII.Факультет управления и информационных технологий. — СПб. : Изд-воСПбГПУ, 2010. — С. 13–15.42. Павлов, В. А. Сравнение эффективности методов автоматическогодоказательстватеорем/В. А. Павлов,В. Г. Пак//МатериалыXXXIXмеждународной научно-практической конференции «Неделя науки СПбГПУ».
—СПб. : Изд-во СПбГПУ, 2011. — С. 62–65.43. Павлов, В. А. Сравнительное исследование методов автоматическогологического вывода для логики предикатов / В. А. Павлов, В. Г. Пак // XL Неделянауки СПбГПУ: материалы международной научно-практической конференции.Часть XVIII. — СПб. : Изд-во Политехн. ун-та, 2011. — С. 10–12.44. Павлов, В. Экспериментальная программа для доказательства теореминтуиционистской логики обратным методом Маслова / В. Павлов, В.
Пак //148Научно-технические ведомости СПбГПУ. Информатика. Телекоммуникации.Управление. — 2015. — № 6. — С. 70–80.45. Павлов, В. Эффективная программная реализация обратного методаМаслова для интуиционистской логики // Научно-технические ведомостиСПбГПУ. Информатика.
Телекоммуникации. Управление. — 2017. — № 1. — С.49–62.46. Петухова, Н. Д. Разработка и оценка числа шагов работы алгоритмоврешения задач логико-предметного распознавания образов с использованиемтактик обратного метода Маслова : дис… канд. физ.-мат. наук : 05.13.17Теоретические основы информатики. — 2016. — 157 с.47. Петухова, Н.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
