Диссертация (1149226), страница 19
Текст из файла (страница 19)
Таммета [139], позволяющее получить более сильную стратегию. Идеясингулярной стратегии для многосукцедентного исчислениядостаточнопроста, но она также не представлена в работах других авторов по обратномуметоду в силу того, что в этих работах используются односукцедентныеисчисления.Доказана полнота каждой из предложенных стратегий, а также любойкомбинации стратегий. Стоит отметить, что во многих публикациях, где описаныстратегии для интуиционистских исчислений обратного метода, доказательстваполноты стратегий даны либо в схематическом виде, либо с отсылкой к другимработам (что можно объяснить ограниченным объемом публикаций).112ГЛАВА 4. АЛГОРИТМ ПОИСКА ВЫВОДА И ПРОГРАММНАЯРЕАЛИЗАЦИЯ ОБРАТНОГО МЕТОДА4.1.
ВведениеВ этой главе в параграфе 4.3 рассматривается вариант алгоритма «givenclause algorithm» [122, 104], адаптированный для поиска вывода в секвенциальныхисчислениях обратного метода. В параграфе 4.4 рассматривается новаяпрограммная реализация обратного метода для интуиционистской логики, вкоторой используется указанный алгоритм. Разработанная программа называетсяWhaleProver, на нее имеется свидетельство о государственной регистрациипрограммы для ЭВМ [48]. В параграфе 4.5 приводятся результаты экспериментовпо сравнению стратегий для обратного метода на задачах из библиотеки ILTPверсии 1.1.2. Эксперименты выполнены с использованием разработаннойпрограммы АЛВ.
В параграфе 4.6 приводится сравнение программы WhaleProverс существующими программами АЛВ для интуиционистской логики первогопорядка, также на задачах из ILTP. В параграфе 4.7 дается описаниеинтерактивного режима программы и приводится пример решенной в этомрежиме задачи из области верификации ПО. В параграфе 4.8 формулируютсявыводы по итогам главы.Основные результаты этой главы изложены в статьях [45, 44, 116, 40].Описание ранних версий программной реализации обратного метода, на основекоторой разработана программа WhaleProver, есть в статьях [114, 42, 43, 41].4.2. Основные определения и обозначенияКроме приведенных в этом параграфе определений, также будутиспользоваться определения и обозначения из глав 1, 2 и 3.В этой главе используются два частных случая стратегии поглощения:стратегии прямого и обратного поглощения.
При прямом поглощении удаляетсяновая секвенция, если она поглощается одной из ранее выведенных секвенций, а113при обратном поглощении удаляетсясуществующая секвенция, котораяпоглощается новой секвенцией.Пусть формуласоответствует соглашению 2.1 или 2.2, авхождением подформулы в . В контексте поиска вывода формулыисчислении обратного метода длиной пути68 до вхожденияформулыявляетсяв некотором(относительно) будем называть число таких различных вхождений подформулформулу , чтоивне совпадает с .Программы, включенные в ILTP, — это шесть программ, детальныерезультаты тестирования которых опубликованы на сайте ILTP [144]: JProver, ftC, ft-Prolog, ileanSeP, ileanTAP, ileanCoP (версия 1.0).4.3. Алгоритм поиска выводаРассмотрим алгоритмпоискавывода,позволяющийкомбинироватьразличные стратегии поиска вывода и применимый не только к исчислениями, но и к другим исчислениям обратного метода, предназначенным длявывода замкнутых формул (при условии использования подходящих стратегий,которые индивидуальны для каждого исчисления).Перед началом работы алгоритма следует зафиксировать используемоеисчисление обратного метода и набор стратегий для этого исчисления.Предполагается, что исходная задача формулируется в виде списка гипотез(нелогических аксиом)ии списка целей, где, а— замкнутые формулы логики первого порядка сравенством.
Задача считается решенной, если найден вывод всех целей из гипотезили установлена невыводимость хотя бы одной из целей (прицельюсчитается формула ). Тогда решение задачи сводится к поиску вывода секвенции(если68, то сукцедент пуст).Понятие «пути» используется по аналогии с –путями из статьи [68].114Пусть— список всех предикатных символов, входящих в— список всех функциональных символов, входящих вобозначим черезформулу, а. Тогда, которая определяетсякак в § 73 книги [13]. Также обозначим черезнекоторый двухместныйпредикатный символ, не совпадающий ни с одним из символов.Подготовительный этап алгоритма состоит из двух шагов. На первом шагесеквенцияпреобразуется к секвенциисеквенциидобавляется формулабез равенства.
Для этого в антецедент, а затем все вхождения формул вида, где и — термы, заменяются предикатом. Полученная секвенциясодержит лишь формулы логики первого порядка без равенства. Из теоремы 41книги [13] следует, что выводимость секвенциив интуиционистскомисчислении предикатов с равенством эквивалентна выводимости секвенциивинтуиционистском исчислении предикатов без равенства.На втором подготовительном шаге задача поиска вывода замкнутойсеквенциисводится к поиску вывода формульного образаЗамкнутая формулаэтой секвенции.очищается: связанные вхождения переменных в формулепереименовываются так, чтобы все кванторы связывали разные переменные.
Принеобходимостиустраняютсякванторы,связывающиенеиспользуемыепеременные. Затем, в зависимости от используемого логического исчисления, изформулы могут устраняться некоторые связки и логические константы.Например, в случае исчисленийконстанты ,иустраняется связкаи логические(как указано в соглашении 2.1), а в случае исчисленийустраняются связки,и логическая константаи(как указано в соглашении2.2). В результате этого подготовительного шага получается формула(или).Одна из основных идей алгоритма заключается в разделении всехучаствующих в выводе секвенций на два списка: активные секвенции (A) ииспользованные секвенции (U).
При этом алгоритм работает так, что списокиспользованных секвенций, как правило, имеет относительно небольшой размер,115а список активных секвенций может разрастаться достаточно сильно. Такжеиспользуется список для временного хранения секвенций (T).Рассмотрим основной алгоритм поиска вывода на примере алгоритма дляисчисления. Для других схожих исчислений (например, для исчисления) алгоритм будет отличаться незначительно. Алгоритм включает в себянесколько шагов:1. Пусть A, U, T — пустые списки.2. Получаем ровно по одной аксиоме исчислениядля каждой различнойпары –атомов, добавляем все аксиомы в список T.3. Удаляем из списка T все секвенции, которые можно удалить в соответствиисо стратегиями УСНП и УСНФ. Для всех оставшихся секвенций из спискаT последовательно выполняем следующую процедуру: применяем ксеквенции правила переименования и нормализации так, чтобы получитьправильную –секвенцию, к полученной секвенции рекурсивно применяемстратегии упрощения и тривиального сокращения, результирующуюсеквенцию добавляем в список A (при необходимости применяем ксеквенции правильное переименование относительно секвенций из спискаA и правило нормализации, как это делается на третьем шаге алгоритма,приведенного в пункте 2.5.4).4.
Если A содержит целевую секвенцию, завершаем работу: формулавыводима (при этом вывод формулы восстанавливаем «снизу вверх»).Иначе переходим к шагу 5.5. Если список A пуст, завершаем работу: формула невыводима. Иначевыбираем из списка A секвенцию. Еслипоглощается какой-либосеквенцией из списка U, удаляемиз списка A (применяется прямоепоглощение) и повторяем шаг 5. Иначе выполняем шаг 6.6. Применяем стратегию обратного поглощения: из списка U удаляем всесеквенции, поглощаемые секвенцией.1167. Полагаем список T равным пустому списку.
Применяем к секвенциивседопустимые правила вывода. Если правило имеет две посылки, то вкачестве второй посылки поочередно подставляем все секвенции из спискаU. Полученные секвенции добавляем в список T, а секвенциюпереносимв список U. Возвращаемся к шагу 3.Отметим, что роль «новой» секвенции из определения стратегий прямого иобратного поглощения (параграф 4.2) в данном алгоритме играет активнаясеквенция, а роль «существующих» секвенций играют секвенции из списка U.Другие активные секвенции не участвуют в работе стратегии поглощения, чтобысократить накладные расходы на проверки поглощения.Поскольку список активных секвенций может иметь большой размер,важную роль в приведенном алгоритме играют критерии выбора активнойсеквенции на шаге 5. Если эти критерии подобраны неудачно, то алгоритм можетбольшую часть времени тратить на обработку и порождение секвенций, которыедалеки от целевой секвенции.В настоящей работе используется стратегия выбора активной секвенции, вкоторой критерии выбора чередуются: несколько раз подряд выбирается активнаясеквенция с минимальным весом, затем один раз выбирается секвенция, котораяраньше других попала в список активных (подобные эвристические стратегиичасто используются в резолютивных программах АЛВ).
Такая стратегиягарантирует, что каждая секвенция, попавшая в список A, рано или поздно будутвыбрана, а соответствующий алгоритм поиска вывода будет удовлетворятькритерию допустимости из замечания 3.4.В качестве весовой функции для секвенций может использоваться,например: сумма длин путей до формул, входящих в секвенцию (определение длиныпути см. в параграфе 4.2); средняя длина пути до формул, входящих в секвенцию; минимальная длина пути до формул, входящих в секвенцию;117 количество символов в текстовой записи секвенции; количество формул, входящих в секвенцию.4.4.
Программа для автоматического поиска вывода WhaleProver4.4.1. Краткое описание программы WhaleProverНа основе приведенного в параграфе 4.3 алгоритма была разработанакомпьютернаяпрограммаWhaleProver,которуюможноприменятьдляавтоматического поиска вывода в интуиционистской логике первого порядка (сравенством) и в интуиционистской логике высказываний.Программаразработанасприменениемобъектно-ориентированногоподхода на языке C++. Выбор языка программирования обусловлен следующимифакторами: гибкость и универсальность языка; возможность управления деталями реализации алгоритма поиска вывода; объектно-ориентированный подход; наличие эффективных реализаций метода резолюций на языках C/C++(можно адаптировать некоторые общеприменимые алгоритмы и структурыданных); кроссплатформенность (т.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
