Диссертация (1149226), страница 23
Текст из файла (страница 23)
Тактика «symmetry». Применима, если текущая цель имеет види— термы. В результате получается новая цель:9. Тактика«auto».Запускаетавтоматическийрежим, где.поискавывода(используемое исчисление, стратегии и лимит времени задаются вконфигурационном файле). При этом решение подзадачисводится кпоиску вывода формулы без равенства, как в параграфе 4.3. В случаеуспешного доказательства текущая подзадача помечается как решенная иудаляется из списка подзадач.10.Тактика «new_lemma». Аргумент — формулаимеет вид.
Пусть текущая подзадача. Если при этом программе в автоматическом режиме (см.тактику «auto») удается доказать секвенцию, то формуладобавляется к существующим гипотезам.Все приведенные тактики корректны: из выводимости всех секвенций,полученных в результате применения какой-либо тактики, следует выводимостьисходной секвенции в интуиционистской логике (с равенством). В то же времяследует учитывать, что не все тактики полны. Например, применив тактику«exists» к выводимой секвенции, можно получить невыводимую секвенцию.После применения очередной тактики программа выводит измененнуюподзадачу на экран (при этом для удобства восприятия выводятся только136последние три гипотезы).
Пользователь может проанализировать результат иприменить следующую тактику. Когда все подзадачи решены, программасообщает об успехе пользователю.В интерактивном режиме удалось решить некоторые задачи, которыепрограмма WhaleProver не может решить в автоматическом режиме. Например,были решены задачи NLP009+1, SET625+3, SWV048+1 и SYN347+1. Из всехпрограмм, приведенных на рисунке 4.1, в автоматическом режиме задачуNLP009+1 могут решить (с ограничением по времени 600 секунд) только двепрограммы: ileanTAP и Imogen. Задачу SET625+3 могут решить толькопрограммы ileanCoP 1.0 и Imogen. Задачи SYN347+1 и SWV048+1 не способнарешить в автоматическом режиме ни одна из программ.Пример 4.1. Рассмотрим, как в интерактивном режиме была решена задачаSWV048+1, которая относится к области верификации ПО. Следует отметить, чтоверификация даже небольших программ является весьма трудной задачей.
Для еекомплексного решения недостаточно использовать только средства логикипервого порядка, однако с помощью более гибких инструментов можно сделатьпредобработкуисвестизадачуверификациикдоказательствунаборапредикатных формул, каждая из которых соответствует проверке определенногочастного свойства исходной программы. Например, задача SWV048+1 былаполученавпроцессеверификацииодногоизпрограммныхпродуктовамериканского космического агентства NASA при выполнении проверки, чтосумма элементов в определенных массивах равна единице78.Задача SWV048+1 содержит 90 формул, включая формулы с равенством.После добавления аксиом для равенства число формул возрастает до 141.Программа не может решить эту задачу в автоматическом режиме за приемлемоевремя из-за быстрорастущего пространства поиска вывода.
Однако анализ задачи78Эта информация содержится в заголовке задачи.137показывает, что в доказательстве достаточно использовать лишь следующие79гипотезы (нелогические аксиомы):где— 0-местный предикат,,и,— функции, а,и— предметные константы (которые интерпретируются как числа 0,1 и -1 соответственно). Последние две формулы — это аксиомы симметричностии транзитивности равенства.Целевая формула в задаче SWV048+1 выглядит так:где,,внутренняя структура формул,,,и предметной константыанеанализируется в рамках данного примера.Чтобы решить задачу в интерактивном режиме программы WhaleProver,можно использовать следующую последовательность действий:1.
Применить тактику «simplify». В результате получится 5 подзадач с целями,вид,,и. Текущая (т. е. первая по списку) подзадача будет иметь, гдесодержит все исходные гипотезы.2. Ввести новую гипотезус помощьютактики «new_lemma». Программа способна вывести формулуизсуществующих гипотез примерно за 3,5 секунды.
В результате текущаяподзадача будет иметь вид79.Здесь и далее обозначения, используемые в библиотеке ILTP при записи формул, приводятся всоответствие с обозначениями, принятыми в настоящей работе.1383. Применить сначала тактику «rewrite» относительно новой гипотезызатемтактику«rewrite_right»относительно, аформулы, входящей в исходный список гипотез.
Введемобозначения:.В,результате подзадача будет иметь вид.4. Ввести новую гипотезус помощью тактики «new_lemma» (доказательство занимает около3,5 секунд).Врезультатетекущаяподзадачабудетиметьвид.5. Применить тактику «rewrite» сначала относительно новой гипотезызатем относительно формулы,.
После этогоприменить тактику «symmetry». В результате подзадача будет иметь вид, где.6. Теперь программа может в автоматическом режиме решить все подзадачи,поэтому достаточно пять раз применить тактику «auto». Доказательствокаждой подзадачи занимает не более 4 секунд.На этом решение задачи SWV048+1 завершено: формула, соответствующаязадаче, выводима в интуиционистской логике.
Анализ тактик, применявшихся винтерактивномрежиме,позволяетпредположить,какиедополнительныеоптимизации могут помочь программе решать задачи такого типа в полностьюавтоматическом режиме. Во-первых, автоматическое применение тактики«simplify» может в ряде случаев упростить задачу поиска вывода. Во-вторых, дляработы с равенствами желательно разработать специализированную стратегию.4.8. ЗаключениеВозможности применения обратного метода в программах АЛВ поканедостаточно изучены. Это хорошо видно из приведенного в главе 1 обзора работпо обратному методу: невелико число статей, посвященных описаниямпрограммных реализаций обратного метода.139В этой главе был рассмотрен алгоритм поиска вывода обратным методомМаслова и разработанная на его основе программа WhaleProver.
Также былоприведено сравнение стратегий поиска вывода для интуиционистских исчисленийобратного метода на задачах различной сложности с использованием рядакритериев, в том числе машинно-независимых. Автор не встречал в литературе пообратному методу подобные сравнительные исследования стратегий.Кроме сравнения стратегий и их комбинаций, результаты экспериментов спрограммой WhaleProver позволяют обнаружить ряд других закономерностей.Так, исчисленияпроигрываютпои, в которых отсутствует связкаоцениваемымпоказателямисчислениям, в среднемисоответственно. Односукцедентные исчисления оказываются предпочтительнеесоответствующих многосукцедентных, однако при использовании оптимальнойкомбинации стратегий их преимущество на рассматриваемой выборке задач нестоль значительно.Результаты тестирования программы WhaleProver на задачах из библиотекиILTP 1.1.2служатпрактическимподтверждениемкорректностисамойпрограммной реализации, алгоритма поиска вывода, а также исчислений истратегий поиска вывода, рассмотренных в главах 2 и 3 настоящей работы.Вкачестведальнейшихперспективможноотметитьповышениеэффективности работы программы с формулами, содержащими равенство, спомощью техник из работ [27, 67, 156].
Также можно использовать свойстванекоторых классов секвенций, для которых выводимость в интуиционистскомисчислении предикатов совпадает с выводимостью в классическом исчислениипредикатов [39]. Другое направление исследований связано с адаптациейстратегий, позволяющих упорядочить применения правил вывода [29, 139, 106].Однако совместимость этих стратегий со стратегиями, используемыми вдиссертационной работе, пока является открытым исследовательским вопросом.Так, Т. Таммет в статье [139] отметил, что стратегия использования обратимостиправил вывода («inversion strategy») в ряде случаев несовместима со стратегией140упрощения («reduction strategy»).
При этом в стратегии фокусировки из [106]также используется обратимость правил вывода. В данном направлениитребуются дополнительные теоретические исследования.Внедрение в программу ряда технических решений, которые используютсяв современных резолютивных программах АЛВ [122, 129], также может помочьрешить новые задачи из ILTP, с которыми у программы сейчас возникаюттрудности. Несмотря на эти трудности, сравнение программы WhaleProver ссуществующими программами АЛВ подтверждает, что при использованииподходящих стратегий и алгоритмов поиска вывода программная реализацияобратного метода для интуиционистской логики первого порядка может быть неменее эффективной, чем реализации табличных методов.
Более того, программаWhaleProver позволяет решить новые задачи относительно существующихпрограмм, а для ряда задач позволяет существенно сократить время решения. Винтерактивном режиме с помощью программы решена новая задача из областиверификации ПО.141ЗАКЛЮЧЕНИЕВ диссертационной работе решена научно-практическая задача, важная дляисследования свойств обратного метода и повышения эффективности егопрактических реализаций. В ходе работы над диссертацией разработан алгоритмпоиска вывода и программа АЛВ на основе обратного метода Маслова, длякоторой характерны гибкость и масштабируемость. Результаты экспериментов нашироком классе задач показали корректность программы АЛВ и ее пригодностьдля решения формализованных технических задач, возникающих в областяхискусственного интеллекта и формальной верификации.Итоги диссертационной работы таковы:1. Выполнено исследование современного состояния предметной области.Выявлены основные тенденции и актуальные задачи в области АЛВ.2.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
