Содержание к диссертации
Введение
Глава 1. Формулировка алгоритма 10
1. Логика ветвящегося времени. Основные понятия 10
2. Построение схемы модели 16
3. Фильтрование схемы модели 24
4. Построение модели 30
Глава 2. Обоснование алгоритма 39
5. Свойства правил алгоритма 39
6. Завершаемость алгоритма 54
7. Корректность алгоритма 63
8. Полнота алгоритма 75
9. Схемы моделей и суммарные схемы моделей 86
Глава 3. Применение алгоритма 116
10. Построение вывода общезначимых формул из аксиом 116
11. Пример применения алгоритма к решению шахматной задачи 136
Заключение 151
Литература 152
- Логика ветвящегося времени. Основные понятия
- Фильтрование схемы модели
- Завершаемость алгоритма
- Пример применения алгоритма к решению шахматной задачи
Введение к работе
Проблема распознавания выполнимости формул в логике имеет большое теоретическое значение и тесно связана с прикладными задачами. Если задача записывается в виде формулы, то выполнимость формулы означает существование решения задачи, а модель, в которой эта формула истинна, даёт решение задачи. Проблема распознавания выполнимости формул в логике высказываний разрешима, однако язык этой логики предоставляет весьма ограниченные выразительные возможности. В то же время в логике предикатов проблема распознавания выполнимости алгоритмически неразрешима, что было доказано Чёрчем [32]. Поиски других достаточно выразительных расширений языка логики высказываний привели к созданию модальных логик [31,38], получаемых путём добавления специальных операторов ("модальностей") и расширения интерпретации пропозициональных переменных. Дальнейшее развитие и комбинирование модальных логик, связанные, в частности, с решением прикладных задач, рассмотрены в монографии [37]. Одной из модальных логик, ориентированных на изучение процессов, происходящих во времени, является так называемая логика ветвящегося времени, известная под названием Ctl - Computational tree logic [36].
В этой логике к пропозициональным связкам добавляются следующие временные: "О" - "в следующий момент", "" - "во всякий момент", "О" - "в некоторый момент", "U" - "до тех пор, пока", а также кванторы "V" и "3", стоящие перед каждой временной связкой (и только перед ней). Истинность формулы определяется в модели: в вершинах связного ориентированного графа, в котором каждой вершине приписаны истинностные значения пропозициональных переменных. Формула называется выполнимой, если существует модель, в начальной вершине которой эта формула истинна. Формула называется общезначимой, если она истинна во всякой модели.
Разрешимость проблемы распознавания выполнимости формул в Ctl доказана в работе [34] путём построения для формулы конечной
структуры (структуры Хинтикки) и её анализа, после которого даётся ответ о выполнимости этой формулы. К распознаванию выполнимости формулы Ctl сформировались два подхода: автоматный и табличный. В первом подходе по формуле строится автомат специального вида, и выполнимость формулы сводится к существованию непустого языка, принимаемого этим автоматом [41]. При таком подходе, однако, не проявляется связь разбора формулы с содержанием задачи, которое отражено в структуре формулы. При табличном подходе применение каждого правила имеет простой содержательный смысл. Наш алгоритм относится ко второму подходу.
Табличный подход основан на методе семантических таблиц, впервые предложенном Бетом [30], и для разрешимых модальных логик изложен в работе [31]. Табличный метод в схематическом виде для Ctl был впервые изложен в работе [34]. Несколько подробнее табличный метод для Ctl был опубликован в работе [36]. Этот метод состоит из построения по формуле конечного табличного графа, его анализа и построения по нему модели в случае выполнимости. Отметим, что в работах [34,36] на граф в модели наложено ограничение в виде тотальности: каждая вершина графа должна иметь сына. Кроме того, некоторые случаи, возникающие, в частности, при построении новых вершин в графе, удалении вершин, проверки подтвержденности так называемых формул-обещаний, в этих работах не рассмотрены. Доказательства корректности, полноты и оценки сложности также даны в виде наброска. В связи с этим использование данного алгоритма, включая построение модели в случае выполнимости, а также доказательство невыполнимости, наталкивается на серьёзные трудности.
Таким образом, оставались актуальными вопросы создания детального табличного алгоритма, его обоснования и применения к решению прикладных задач. Кроме того, согласно работам Эмерсона [34,36], табличные графы имеют вообще говоря экспоненциальное число вершин, поэтому актуален вопрос: всегда ли для ответа на вопрос о выполнимости формулы необходимо полностью строить эту структуру, или существуют случаи, когда достаточно некоторого её
фрагмента?
Система аксиом и правил вывода для логики ветвящегося времени вместе с доказательством её полноты приведены в работе [34]. Подстановка формул в эти аксиомы и использование правил вывода теоретически позволяют перечислить все возможные выводы общезначимых формул из аксиом. Однако такой путь практически не даёт вывода данной произвольной формулы из этих аксиом. В связи с этим для Ctl также возникает вопрос описания эффективного метода построения вывода всякой общезначимой формулы из аксиом.
В настоящей работе создан и детально изложен алгоритм распознавания выполнимости формул логики ветвящегося времени, основанный на построении так называемой схемы модели. Схема модели является уточнением табличного графа путём выделения положительных и отрицательных формул, введения специальных пометок для формул и вершин, а также характеристических формул (х.ф.) вершин. Для правил построения схемы модели и её* дальнейших преобразований установлен ряд соотношений между х.ф., с помощью которых, в частности, доказаны корректность и полнота алгоритма распознавания выполнимости. В случае применения данного алгоритма к отрицанию общезначимой формулы для схемы модели установлены соотношения между отрицаниями х.ф. её вершин. С использованием этих соотношений сформулирован эффективный алгоритм построения вывода двойного отрицания данной общезначимой формулы и, следовательно, самой общезначимой формулы из аксиом.
По классификации А.А.Ляпунова и С.В.Яблонского [10,26] шахматная позиция является одной из управляющих систем (У.С), обладающей структурой и функционированием. Таким образом, проблему нахождения решения шахматной задачи можно рассматривать как пример синтеза У.С. В качестве примера такой задачи нами выбран этюд К.Эберса [15], являющийся одной из самых сложных задач, относящихся к шахматной теории систем полей соотоветствия [24]. Условие этой задачи записано в виде конъюнкции трёх формул: формулы, соответствующей начальным положениям фигур, форму-
лы, описывающей возможные ходы, и формулы-цели, достижение которой равносильно получению требуемого результата. Применение авторского алгоритма распознавания выполнимости к этой формуле дало модель, по которой получено полное решение данного этюда - первый ход и дальнейшие ответы на любой из ходов соперника в каждой из возникающих позиций.
Настоящая диссертация состоит из введения, трёх глав, разбитых на 11 параграфов, заключеЕшя и списка литературы.
В первой главе формулируется алгоритм распознавания выполнимости формул логики ветвящегося времени. В 1 вводятся основные понятия для логики ветвящегося времени. При этом в 1 и последующих параграфах рассматривается общий случай моделей - связные ориентированные графы с выделенной начальной вершиной, на которые не наложено ограничение в виде тотальности. Алгоритм распознавания выполнимости содержится в 2-4 и состоит из трёх частей. В 2 даётся определение схемы модели и формулируется первая часть алгоритма - построение схемы модели. Второй частью алгоритма, изложенной в 3, является фильтрование схемы модели, состоящее в проверке подтверждённости в вершинах схемы модели так называемых формул-обещаний. Третья часть алгоритма изложена в 4 и состоит в построении для формулы модели в случае её существования, т.е. в случае выполнимости формулы.
В главе 2 доказывается ряд теорем об алгоритме распознавания выполнимости формул из главы 1. В 5 устанавливаются свойства правил алгоритма для х.ф. вершин, к которым эти правила применяются. В 6 доказывается теорема о завершаемости работы алгоритма за конечное число шагов. В 7 доказывается теорема о корректности работы алгоритма (теорема 7.3). Эта теорема утверждает, что в найденной алгоритмом модели для исследуемой формулы эта формула истинна. Отсюда следует, что если для формулы 0 алгоритм даёт ответ "0 выполнима", то этот ответ всегда является верным.
В 8 доказывается, что для исследуемой формулы 0 ответ алгоритма "0 не выполнима" также всегда является верным, т.е. в этом
случае формула 0 действительно не выполнима в соответствии с определениями 1. С учётом теоремы о завершаемости работы алгоритма отсюда получается доказательство теоремы о полноте алгоритма (теоремы 8.3), утверждающей, что если формула 0 выполнима, то некоторая модель, в которой эта формула истинна, будет найдена алгоритмом. Из теорем о корректности и полноте алгоритма получается следствие (следствие 8.1), которое заключается в том, что если формула истинна в некоторой бесконечной модели, то она истинна и в некоторой конечной модели.
Наконец, в 9 устанавливается в определённом смысле единственность схемы модели и суммарной схемы модели, введённой в 2 п.2.6 и соответствующей табличному графу в работе Эмерсона [36]. Также в этом параграфе доказывается нестрогое включение первой из схем моделей во вторую и приводятся примеры классов формул, для которых это включение строгое. Отсюда следует, что алгоритм распознавания выполнимости формул из главы 1, основанный на построении схемы модели, работает либо быстрее, либо за то же число шагов, что и алгоритм Эмерсона, основанный на построении табличного графа.
В главе 3 рассмотривается теоретическое и практическое применение сформулированного в главе 1 алгоритма. В 10 рассматривается теоретическое применение - формулируется эффективный алгоритм построения вывода общезначимых формул из аксиом. Для данной общезначимой формулы рассматривается задача распознавания выполнимости её отрицания. Попытка построить для такой формулы модель приводит к неудаче, однако накопленная в построенной схеме модели информация используется для вывода двойного отрицания исходной формулы. Этот процесс начинается с вывода отрицаний х.ф. концевых вершин, а также отрицаний х.ф. вершин, содержащих неподтверждённые обещания, и продолжается "снизу вверх" вплоть до вывода отрицания х.ф. начальной вершины, совпадающей с двойным отрицанием данной общезначимой формулы. Наконец, из вывода двойного отрицания исходной общезначимой формулы получается вывод её самой. Для данного эффективного алгоритма постро-
ения вывода общезначимых формул из аксиом доказывается теорема о полноте (теорема 10.1): если формула Э общезначима, то она выводима, а также теорема о корректности (теорема 10.2): если формула 0 выводима, то она общезначима. С использованием этих теорем получается второе доказательство теоремы о полноте (теоремы 8.3) для алгоритма распознавания выполнимости формул.
В 11 рассматривается практическое применение алгоритма, состоящее в записи прикладной задачи в виде формулы и построении модели, по которой получается решение задачи. Как уже отмечалось выше, в качестве примера решения прикладной задачи нами выбрано решение шахматного этюда Эберса. В этюде Эберса ход белых: могут ли они сделать ничью, и если могут, то как им для этого надо играть? По этой задаче выписана формула 0 (11.4), имеющая вид: Init Л Rules Л Aim, где формула Init соответствует начальной позиции, формула Rules соответствует правилам игры, а формула Aim (11.3) соответствует цели (белых), заключающейся в данном этюде в контролировании ключевых полей, достижение которой равносильно решению задачи. Путём применения алгоритма распознавания выполнимости из главы 1 установлено, что формула 0 выполнима, построена модель М (таблицы 11.1 и 11.2) и доказано, что формула 0 истинна в этой модели. В построенной модели М для формулы 0 вершины соответствуют позициям, начальная вершина - начальной позиции. Дуга из одной вершины в другую соответствует изменению позиции вследствие сделанного хода, который однозначно получается по отличию истинных пропозициональных переменных в этих вершинах. В модели М вершины, соответствующие позициям, в которых ходят белые, и вершины, соответствующие позициям, в которых ходят чёрные, чередуются. Причём из первых выходит ровно одна дуга, а из вторых - число дуг, равное числу возможных ходов чёрных в возникшей позиции. Таким образом, все вершины первого вида с учётом изменений переменных в сыне каждой из них дают полное решение задачи - все пары: (встречающаяся позиция) - ход белых, которое выписано в п.11.7. В п.11.8 показывается трудность нахождения чис-
то шахматного решения и трудоёмкость обнаружения ошибочности неправильного хода белых. Наконец, в п.11.9 указывается метод построения по шахматной задаче и формуле 0 формулы 0' (называемой двойственной к формуле 0), выполнимость которой равносильна невозможности достижения нами требуемого результата. При этом по модели, в которой формула 0' истинна, аналогично п.11.7 находится стратегия противника, которая не позволяет достичь цели ни при какой нашей игре. Таким образом, исследование нашим алгоритмом этих двух формул, ровно одна из которых выполнима, позволяет в рамках поставленной цели отвечать на вопрос о существовании решения и получать либо полное решение в случае его существования, либо конструктивное (конкретное и исчерпывающее) доказательство его отсутствия.
В заключении формулируются основные результаты диссертации, изложенные в работах [17-22].
Логика ветвящегося времени. Основные понятия
В первой главе формулируется алгоритм распознавания выполнимости формул логики ветвящегося времени. В 1 вводятся основные понятия для логики ветвящегося времени. При этом в 1 и последующих параграфах рассматривается общий случай моделей - связные ориентированные графы с выделенной начальной вершиной, на которые не наложено ограничение в виде тотальности. Алгоритм распознавания выполнимости содержится в 2-4 и состоит из трёх частей. В 2 даётся определение схемы модели и формулируется первая часть алгоритма - построение схемы модели. Второй частью алгоритма, изложенной в 3, является фильтрование схемы модели, состоящее в проверке подтверждённости в вершинах схемы модели так называемых формул-обещаний. Третья часть алгоритма изложена в 4 и состоит в построении для формулы модели в случае её существования, т.е. в случае выполнимости формулы.
В главе 2 доказывается ряд теорем об алгоритме распознавания выполнимости формул из главы 1. В 5 устанавливаются свойства правил алгоритма для х.ф. вершин, к которым эти правила применяются. В 6 доказывается теорема о завершаемости работы алгоритма за конечное число шагов. В 7 доказывается теорема о корректности работы алгоритма (теорема 7.3). Эта теорема утверждает, что в найденной алгоритмом модели для исследуемой формулы эта формула истинна. Отсюда следует, что если для формулы 0 алгоритм даёт ответ "0 выполнима", то этот ответ всегда является верным.
В 8 доказывается, что для исследуемой формулы 0 ответ алгоритма "0 не выполнима" также всегда является верным, т.е. в этом случае формула 0 действительно не выполнима в соответствии с определениями 1. С учётом теоремы о завершаемости работы алгоритма отсюда получается доказательство теоремы о полноте алгоритма (теоремы 8.3), утверждающей, что если формула 0 выполнима, то некоторая модель, в которой эта формула истинна, будет найдена алгоритмом. Из теорем о корректности и полноте алгоритма получается следствие (следствие 8.1), которое заключается в том, что если формула истинна в некоторой бесконечной модели, то она истинна и в некоторой конечной модели.
Наконец, в 9 устанавливается в определённом смысле единственность схемы модели и суммарной схемы модели, введённой в 2 п.2.6 и соответствующей табличному графу в работе Эмерсона [36]. Также в этом параграфе доказывается нестрогое включение первой из схем моделей во вторую и приводятся примеры классов формул, для которых это включение строгое. Отсюда следует, что алгоритм распознавания выполнимости формул из главы 1, основанный на построении схемы модели, работает либо быстрее, либо за то же число шагов, что и алгоритм Эмерсона, основанный на построении табличного графа.
В главе 3 рассмотривается теоретическое и практическое применение сформулированного в главе 1 алгоритма. В 10 рассматривается теоретическое применение - формулируется эффективный алгоритм построения вывода общезначимых формул из аксиом. Для данной общезначимой формулы рассматривается задача распознавания выполнимости её отрицания. Попытка построить для такой формулы модель приводит к неудаче, однако накопленная в построенной схеме модели информация используется для вывода двойного отрицания исходной формулы. Этот процесс начинается с вывода отрицаний х.ф. концевых вершин, а также отрицаний х.ф. вершин, содержащих неподтверждённые обещания, и продолжается "снизу вверх" вплоть до вывода отрицания х.ф. начальной вершины, совпадающей с двойным отрицанием данной общезначимой формулы. Наконец, из вывода двойного отрицания исходной общезначимой формулы получается вывод её самой. Для данного эффективного алгоритма постро ения вывода общезначимых формул из аксиом доказывается теорема о полноте (теорема 10.1): если формула Э общезначима, то она выводима, а также теорема о корректности (теорема 10.2): если формула 0 выводима, то она общезначима. С использованием этих теорем получается второе доказательство теоремы о полноте (теоремы 8.3) для алгоритма распознавания выполнимости формул.
В 11 рассматривается практическое применение алгоритма, состоящее в записи прикладной задачи в виде формулы и построении модели, по которой получается решение задачи. Как уже отмечалось выше, в качестве примера решения прикладной задачи нами выбрано решение шахматного этюда Эберса. В этюде Эберса ход белых: могут ли они сделать ничью, и если могут, то как им для этого надо играть? По этой задаче выписана формула 0 (11.4), имеющая вид: Init Л Rules Л Aim, где формула Init соответствует начальной позиции, формула Rules соответствует правилам игры, а формула Aim (11.3) соответствует цели (белых), заключающейся в данном этюде в контролировании ключевых полей, достижение которой равносильно решению задачи. Путём применения алгоритма распознавания выполнимости из главы 1 установлено, что формула 0 выполнима, построена модель М (таблицы 11.1 и 11.2) и доказано, что формула 0 истинна в этой модели. В построенной модели М для формулы 0 вершины соответствуют позициям, начальная вершина - начальной позиции. Дуга из одной вершины в другую соответствует изменению позиции вследствие сделанного хода, который однозначно получается по отличию истинных пропозициональных переменных в этих вершинах. В модели М вершины, соответствующие позициям, в которых ходят белые, и вершины, соответствующие позициям, в которых ходят чёрные, чередуются. Причём из первых выходит ровно одна дуга, а из вторых - число дуг, равное числу возможных ходов чёрных в возникшей позиции. Таким образом, все вершины первого вида с учётом изменений переменных в сыне каждой из них дают полное решение задачи - все пары: (встречающаяся позиция) - ход белых, которое выписано в п.11.7. В п.11.8 показывается трудность нахождения чисто шахматного решения и трудоёмкость обнаружения ошибочности неправильного хода белых. Наконец, в п.11.9 указывается метод построения по шахматной задаче и формуле 0 формулы 0 (называемой двойственной к формуле 0), выполнимость которой равносильна невозможности достижения нами требуемого результата. При этом по модели, в которой формула 0 истинна, аналогично п.11.7 находится стратегия противника, которая не позволяет достичь цели ни при какой нашей игре. Таким образом, исследование нашим алгоритмом этих двух формул, ровно одна из которых выполнима, позволяет в рамках поставленной цели отвечать на вопрос о существовании решения и получать либо полное решение в случае его существования, либо конструктивное (конкретное и исчерпывающее) доказательство его отсутствия. В заключении формулируются основные результаты диссертации, изложенные в работах [17-22].
Фильтрование схемы модели
В начале исследования формулы 0 на выполнимость схема модели G состоит из вершин Do, Со, дуги (DQ,CQ), где DQ = {0}, DQ = 0, Cf = {0}, CQ — 0. Такая схема модели называется начальной. Схема модели называется Х-размеченной [Т-размеченной], если её начальная вершина Х-помечена [Т-помечена]. Схема модели G называется размеченной, если она 1) Х-размечена; либо 2) Т-размечена; или 3) каждая концевая вершина в G помечена или не является свободно достижимой.
Построение размеченной схемы модели начинается с начальной схемы модели и состоит в применении указанных ниже правил 1-6 в порядке их следования. Для схемы модели каждое правило применяется к некоторой непомеченной концевой свободно достижимой основной вершине d и даёт новую схему модели.
Как обычно, оператор ";=" означает, что левой части оператора присваивается значение, равное правой части оператора, а В{ = В? означает, что Bf = В? и Bf = Bf. Если В{ = By, то вершины ВІ и В? называются равными. Всюду в дальнейшем в случае записи Cf := Cf\J{ p} [Cf := Cf\J{(p}] формула (p добавляется во множество С [Cf] тогда и только тогда, когда множество С [Cf] не содержит ни формулу ц % ни формулу (р-к. Будем говорить, что формула (р) где р Є С [ р Є Cf] помечается знаком , если Cf := {Cf \ip)\J {(р } [Cf:=(Cf\cp)u{ p }].
Зафиксируем следующий порядок применения правил 1-6 к основным вершинам в схеме модели. Пусть эти правила применяются к основным вершинам в порядке их появления в схеме модели. 1. Правило противоречия. Условие применения правила: 1) Т Є Cf; или 2) X Є Cf; или 3) существует такая формула 0, что в или 6-к принадлежит Cf и в или в принадлежит Cf. Применение правила состоит в выполнении рекурсивной процедуры Х-разметки с индексом О для вершины СІ. Процедура JL-размєтки с индексом щ для вершины С{. Вершине СІ приписывается верхний индекс Хп;. Если каждый родитель D{ вершины С{ JL-помечен или имеет сына без Х-пометки, то конец процедуры Х-разметки. Иначе каждому родителю D{k вершины С , не имеющему Х-пометки, но все сыновья которого X-помечены, приписывается верхний индекс J_nIt, где щк есть максимальный индекс Х-пометок сыновей вершины Dik. Если теперь каждый родитель каждой такой вершины Dik Х-помечен, то конец процедуры Х-разметки. Иначе выделяется каждая вершина Cj без Х-пометки, являющаяся родителем хотя бы одной из таких вершин D(k. Пусть rij - минимальный из индексов Х-пометок вершин, являющихся сыновьями вершины Cj. Тогда процедура Х-разметки выполняется с индексом rij + 1 для каждой такой вершины Cj. Конец процедуры Х-разметки. Комментарий. Ниже (5, п.5.3) будет показано, что если вершина В{ становится Х-помеченной, то её х.ф. не выполнима. 2. Правило завершения. Условие применения правила: 1) ХС; = Т; или 2) xCi = "-L; или 3) каждая непомеченная формула из Cf является пропозициональной переменной или формулой вида VO , и каждая непомеченная формула из Cf является пропозициональной переменной или формулой вида 30 . Применение правила состоит в выполнении рекурсивной процедуры Т-разметки с индексом 0 для вершины С{. Процедура Т-разметки с индексом щ для вершины С{. Вершине d приписывается верхний индекс Тщ. Если каждый родитель Di вершины СІ Т-помечен, то конец процедуры Т-разметки. Иначе каждому родителю Dik вершины Cj, не имеющему Т-пометки, приписываются верхние индексы Тщ + 1,(7,-. Если теперь каждый родитель вершин D{k Т-помечен или имеет сына без Т-пометки, то конец процедуры Т-разметки. Иначе выделяется каждая вершина Cj без Т-пометки, имеющая только Т-помеченных сыновей, среди которых есть хотя бы одна из таких вершин D{k. Пусть Djl п п,..., Djm J"" 3m - все сыновья такой вершины Су, и rij = тажі тгг;л, где rijh - индекс Т-пометки вершины Djh. Тогда процедура Т-разметки выполняется с индексом rij для каждой из выделенных вершин Cj. Конец процедуры Т-разметки. Комментарий, Очевидно, что C HCf = 0, так как иначе было бы применено правило 1; а всякая формула вида VO » или — 30ф является истинной в концевой вершине модели. Ниже (5, п.5.4) будет показано, что если вершина J3j становится Т-помеченной, то её х.ф. выполнима. 3. Правило эквивалентности. Условие применения правила: а) Є = Уп р е Ct, b) в = BUtp е Ct, с) 0 = УО р Є Cf, d) в = ЗО? Є Ct, е) в =: V(y U ) Є Cf, f) 0 = 3(cp У ) Є Ct. В случаях g) 1) условие аналогично a)-f) для Cf. Применение правила состоит в пометке формулы в знаком и введении формулы 6 для условий а)-1) соответственно: a)[g)] в = {(р Л VOVD ), b)[h)] в - ( р Л (303Пір V VO_L)), c)[i)] в = (ip V (VOVOy Л ЗОТ)), d)[j)] 6 = ( pV ЗОЗО ), e)[k)] 0 = ( V (( Л V0V(v У V)) А ЗОТ)), f)[l)] б = (ф V (у Л 303( U ф))). Далее в случаях a)-f) Cf = Cf U{0 }, в случаях g)-h) С := Cf U{0 }, а затем происходит возможное отождествление вершины С . Здесь и правилах 4-6 отождествление вершины Ct- состоит в следующем. Если Di - родитель вершины С;, и в схеме модели существует вершина Су, равная вершине С І, то проводится дуга (D{, Cj) (в случае её отсутствия), а дуга (-Df,Ci) и вершина СІ удаляются. Теперь если вершина Cj помечена с индексом rij пометки, то для неё выполняется соответствующая процедура разметки с индексом rtj. Комментарий. Данные эквивалентности в = в получаются на основании леммы 5.1 (5, п.5.1). Систематическое их применение позволяет в дальнейшем рассматривать только формулы с главной пропозициональной связкой, а также формулы вида VO0 и 30 .
Завершаемость алгоритма
В этом пункте устанавливается свойство правила эквивалентности - правила 3. Это правило применяется к формуле 0, принадлежащей множеству положительных либо отрицательных формул в вершине СІ. Оно состоит в пометке этой формулы знаком и добавлении формулы в в случае её отсутствия в соответствующее множество формул. Формула в имеет один из следующих видов: a) Vdy , , b) ЕЮуэ, с) VO , d) ЗОір, е) V(y U ф), f) 3( р О ф). Тогда соответствующая ей формула 6 имеет вид: a) (i AVOVn )} b) (9?A(303ny VVOX)), с) ( V(VOVO A30T)), d) ( pV3030 p), є) (ф V (((р Л VOV(v? U ф)) А ЗОТ)), f) (ф V ( р Л ВОЗ( р Ъф))). Свойство правила эквивалентности устанавливается леммой 5-ій заключается в общезначимости формулы 9 = 9 . Лемма 5.1. Формулы a) VDy? = {(р A VOVD ), b) ЗП р = (ip А (ЗОЗПу? V VOX)), с) V V = ( р V (VOVOy А ЗОТ)), d) ЗОір {tpV 3030 р), є) 4( рї}ф) = (фЧ(((рЛЧОІ( рПф)) ЛЗОТ))у f) 3( риф) = (ф V (ip А ВОЗ( р U ф))) общезначимы. Доказательство. Требуется установить общезначимость формулы 6 = 6 для каждого из случаев a)-f). Для этого докажем общезначимость формул 1) (6 — 6 ) и 2) (6 — в) в каждом из этих б случаев. а.1) Допустим, что формула (\/Оср — (у? А УО\/П )) не общезначима. Тогда существует модель М, в начальной вершине которой эта формула не истинна, т.е. М,щ (\/П р — (у? A VOVn )). Отсюда следует М, щ \= VDy? и М, щ И1 У или ио И1 VOVd . Так как М, u0 f= \/П р, то М", щ \= (р. По определению истинности формулы в вершине модели, из М, щ VOVD p следует, что у вершины Uo есть сын щ} в котором М,щ \jt= VDyj. Это означает, что в некотором полном пути с началом в вершине щ существует вершина UJ, в которой формула ір не истинна, т.е. M,Uj $= (р. Однако последнее в силу достижимости вершины Uj из щ противоречит М, UQ \= ЧПір. а.2) Допустим, что формула (((р Л VOVd ) — \/П р) не общезначима. Тогда существует модель М, в которой М, щ \= р, М, щ = VOVn o и М, «о VDyj. Если у вершины щ сыновей нет, то из М, щ = VO следует М, «о И= V, что сразу даёт противоречие. Если же вершина «о сыновей имеет, то в силу М, щ \= \/0$0(р для каждого её сына Uj верно M,Uj \= WOtp. Последнее означает, что для всякого полного пути с началом в вершине Uj во всякой его вершине истинна формула tp. Но в силу произвольности выбора сына Uj вершины щ и М, щ \= (р это означает, что и для всякого полного пути с началом в вершине но во всякой его вершине истинна формула р. Последнее противоречит М, щ \/= VD p. Общезначимость формулы а) доказана.
Допустим, что формула {ЗО р — ( /? Л {ЗОЗОір V VOJL))) не общезначима. Тогда существует модель М, в которой М, щ = ЗПу?, а также М, UQ р ИЛИ М, гі0 ЗОЗп шМ,и0 [ VOJ_. Из М, щ \=3Uip следует М, щ = (р. Если теперь у вершины щ нет сыновей, то М, щ \= VOX, откуда сразу получается противоречие. Если же у вершины щ сыновья есть, то из Му щ $= 3030 р следует, что для каждого её сына Uj верно M,Uj \ 30 р, Последнее означает, что не существует полного пути с началом в вершине Uj, в каждой вершине которого формула (р истинна. Но в силу произвольности выбора сына Uj вершины щ это означает, что не существует и полного пути с началом в вершине щ в каждой вершине которого формула р истинна. А это противоречит М,щ \= ЗП(р.
Допустим, что формула {{ср А {ЗОЗП(р V VOJ.)) — ЗПір) не общезначима. Тогда существует модель М, в которой М,щ = (р и М, щ \= ЗОЗОїр или М,щ \= VO-L, а также М, щ = ЗП(р. Если у вершины щ нет сыновей, то из М, щ 30 р следует М, щ $= (р, откуда сразу получается противоречие. Если же вершина щ сыновей имеет, то М, щ \fc VO-L и, следовательно, верно М,щ )= ЗОЗП(р. Тогда существует сын ui вершины «о, для которого верно М, щ \= ЗПір, Т.е. существует полный путь с началом в вершине ui, в каждой вершине которого формула р истинна. Но тогда существует и полный путь с началом в вершине щ, в каждой вершине которого формула р истинна. Последнее противоречит М, щ ЗО (р. Общезначимость формулы Ъ) доказана.
Допустим, что формула (VO p - ( р V (VOVOy? Л ЗОТ))) не общезначима. Тогда существует модель М, в которой М,щ (= VO p, а также М,щ \ р и М, щ \fc VOVO9? или М,щ $= ЗОТ. Если теперь у вершины щ нет сыновей, то из М, щ = VO / следует М, щ \= рг откуда сразу получается противоречие. Если же у вершины щ сыновья есть, то М,щ \= ЗОТ и, следовательно, М, щ VOVO p. Последнее означает, что существует сын щ вершины щ, для которого верно М, щ Y= VO \ Таким образом, не верно, что во всяком полном пути с началом в вершине щ существует вершина, в которой формула р истинна. Но тогда не верно, что и во всяком полном пути с началом в вершине щ существует вершина, в которой формула р истинна. А это противоречит М, щ \= VO . с.2) Допустим, что формула (( р V (VOVOc/з Л ЗОТ)) — VO p) не общезначима. Тогда существует модель М, в которой М, щ\= р или М,щ [= VOVO и М,щ (= ЗОТ, а также М,щ \t= VOp. Из М,щ [ УО р Следует М, UQ \ (р. ЕСЛИ Теперь у ВерШИНЫ UQ НЄТ СЫНОВеЙ, то М, щ }=ЗОТ, откуда сразу получается противоречие. Если же вершина щ сыновей имеет, то в силу М, щ \= VOVOy? для каждого сына Uj вершины щ верно M,Uj \= ЧОц . Т.е. во всяком полном пути с началом в вершине и;-, существует вершина, в которой формула ср истинна. Но тогда в силу произвольности выбора сына Uj вершины щ и во всяком полном пути с началом в вершине щ существует вершина, в которой формула ср истинна. Последнее противоречит М, щ УО р. Общезначимость формулы с) доказана. d.l) Допустим, что формула (ЗОїр —у [ip V ЗОЗОу?)) не общезначима. Тогда существует модель М, в которой М, щ = ЗОуз, М, щ )/= Р и М, щ ЗОЗОу . Если у вершины щ сыновей нет, то из М, щ \= ЭО(р следует М, щ \= ip, что сразу даёт противоречие. Если же вершина сыновей имеет, то в силу М, щ р ЗОЗО для каждого её сына Uj верно М, Uj р 3 р. Таким образом, не верно, что для некоторого полного пути с началом в вершине Uj существует вершина, в которой истинна формула р. Но тогда в силу произвольности выбора сына Uj вершины щ и М,щ = Р также не верно, что и для некоторого полного пути с началом в вершине щ существует вершина, в которой истинна формула р. Последнее противоречит М,щ р 30 р. d.2) Допустим, что формула ((у? V 303 р) — ВО(р) не общезначима. Тогда существует модель М, в которой М, щ p. ip или М, щ р ЗОЗО с, а также М, щ р 30(р. Так как М, щ р ЗОс/?, то М, щ р р. По определению истинности формулы в вершине модели, из М, «о р ЭОЗО(/э следует, что у вершины щ есть сын гіі, в котором М, Uj. р 30 р. Это означает, что в некотором полном пути с началом в вершине щ существует вершина Uj, в которой формула (р истинна, т.е. М, Uj f= р. однако последнее в силу достижимости вершины Uj из щ противоречит М щ р ЗО о. Общезначимость формулы d) доказана. е.1) Допустим, что формула (V( p & ф) - (ф V (( Л VOV( У ф)) Л ЗОТ))) не общезначима. Тогда существует модель М, в которой верно М,щ рУ( О ),М,и0 р иМ,и0 p(( AVOV( t3 ))A30T). Из последнего следует М,щ р (р, или М, uo р VOV( p О -0), или М, uo р ЗОТ. Если теперь у вершины uo нет сыновей, то из М, uo р V((/? 5 -0) следует М, щ \= ф, откуда сразу получается противоречие. Если же у вершины щ сыновья есть, то М,щ р ЗОТ и, следовательно, верно М, щ р или М, щ р VOV(v U ). Если М, uo р , то с учётом М, WQ р 0 получается противоречие с M,UQ 1= V(v J ф). Если же М, uo р VOV(y?t3 0), то существует сын и і вершины wo, для которого верно М,щ р V( p О 0). Таким образом, не верно, что во всяком полном пути с началом в вершине щ существует вершина, в которой истинна формула ф,а,в каждой ей предшествующей вершине истинна формула ip. Но тогда не верно, что и во всяком полном пути с началом в вершине WQ существует вершина, в которой истинна формула фу а в каждой ей предшествующей вершине истинна формула ip. Это противоречит М}щ р V((p О ф).
Пример применения алгоритма к решению шахматной задачи
Доказательство. Длины добавляемых в случаях 1-3 в Н(0) формул уменьшаются. Для формулы, добавляемой в каждом из случаев 4-9, затем происходит не более 3 применений п.1 индукционного перехода. При этом число добавляемых формул не более 6, и не более чем для 4 формул индукционный переход ещё не выполнялся. Эти 4 формулы могут быть следующего вида: (р или ф - тогда длина каждой из них меньше длины формулы в; ЗОТ или VOX — тогда из них могут быть добавлены не более 2 формул; ЗО0 или VO0 — тогда в силу п.З новых добавлений нет, так как к формуле в индукционный переход уже применялся. Все случаи разобраны. В силу конечности длины формулы в множество Н(0) конечно. Лемма доказана.
Доказательство. Число различных множеств Df (D ) не превосходит 2Ія(е)І, поэтому число различных пар Df, D f не превосходит 22 1я(0)1. В соответствии с правилом 6 все временные вершины различны, поэтому их число также не превосходит 22 я(е)1. Число различных множеств Cf (С[) не превосходит З я 0 , поскольку для каждой формулы в Є H(Q) возможно 3 варианта: в Є С , 9-к Є С , в Cf {в Є Сг", 0 Cf, в С ). Отсюда в силу отождествления, также выполняемого за конечное число шагов, число основных вершин не превосходит 32" я 0)!. Лемма доказана.
Доказательство. По определению вершина і?, называется Х-сво-бодно [Т-свободно] достижимой, если в G существует цепь, идущая из начальной вершины в вершину В каждая вершина которой не является Х-помеченной [Т-помеченной]. В силу леммы 6.3 и наличия не более одной дуги, ведущей из одной вершины в другую, число цепей, ведущих из начальной вершины в вершину В конечно, а так же конечно число вершин в каждой из них. Поэтому число проверок вершин на Х-помеченность [Т-помеченность] также конечно. Лемма доказана.
Лемма 6.5. Рекурсивная процедура Х-разметки [Т-разметки] из правила 1 [2] выполняется за конечное число шагов. Доказательство. Заметим, что выяснение является ли данная вершина полезной [соответственно /Т-вершиной] сводится к распознаванию ее Х-ев обод ной [Т-свободной] достижимости и выполняется в силу леммы 6.4 за конечное число шагов. Выполнение рекурсивной процедуры Х-разметки [Т-разметки] для одной вершины СІ С индексом щ происходит за конечное число шагов. Число таких вершин в силу леммы 6.3 конечно и уменьшается после каждого выполнения процедуры Х-разметки [Т-разметки] для основной вершины с соответствующим индексом её Х-пометки [Т-пометки]. Поэтому и рекурсивная процедура Х-разметки [Т-разметки] из правила 1 [правила 2] выполняется за конечное число шагов. Лемма доказана. Лемма 6.6. Каждое из правил 1-6 выполняется за конечное число шагов.
Доказательство. Для правил 1 и 2 утверждение леммы следует из лемм 6.1,6.2 и 6.5. Каждое из правил 3-4 выполняется не более чем за три шага. В каждом пункте правила 5 выполняется не более чем 2 if(0) по копированию формул в новую вершину и не более 3 шагов, состоящих в пометке формулы знаком и двух добавлений. Число временных вершин} становящихся сыновьями вершины СІ в правиле 6, не превосходит 2 [Л(@). Число сыновей данных временных вершин, получаемых в этом правиле, также не превосходит указанной оценки. Поэтому каждое из правил 1-6 выполняется за конечное число шагов. Лемма доказана. Лемма 6.7. Все правила, применяемые к сыновьям произвольной временной вершины Z?j, выполняются за конечное число шагов.
Доказательство. Сразу после своего появления в схеме модели вершина Di имеет единственного сына С;, причём СІ = D{. Число формул во множестве Cf (Ctr) не превосходит iJ(0), а каждое пра вило либо не увеличивает число сыновей вершины D{, либо (см. правило 5) добавляет еще одного сына. Поэтому число сыновей вершины Di конечно и не превосходит 22 1Я 0)1. Каждое правило применяется к каждому сыну вершины D{ либо один раз (правила 1,2 и 6), либо не более 2 І7(0) раз. Поэтому в силу леммы 6.6 все правила, применяемые к сыновьям произвольной временной вершины .Dj, выполняются за конечное число шагов. Лемма доказана.
Лемма 6.8. Размеченная схема модели получается из начальной за конечное число шагов.
Доказательство. В силу леммы 6.3 число временных вершин в схеме модели конечно. А из леммы 6.7 следует, что для сыновей каждой временной вершины все правила выполняются за конечное число шагов. Поэтому после конечного числа шагов либо начальная вершина становится помеченной, либо в схеме модели не остается свободно достижимых концевых вершин, и тогда размеченная схема модели построена. Лемма доказана.
Лемма 6.9. Приведение размеченной схемы модели к завершенной выполняется за конечное число шагов. Доказательство следует из лемм 6.3 и 6.4. Теорема 6.1 (первая теорема о завершаемости). Для любой формулы 0 завершённая схема модели получается из начальной за конечное число шагов. Доказательство следует из лемм 6.8 и 6.9. Теорема доказана. Для Е-схемы модели, размеченнной S-схемы модели и завершённой S-схемы модели леммы 6.1-6.9 и их доказательства остаются справедливыми практически без изменений. В лемме 6.4 _1_-свобод-ная [Т-свободная] достижимость заменяется на -L-помеченность [Т-помеченность]. А в доказательстве леммы 6.8 свободно достижимые концевые вершины заменяются на концевые непомеченные. Таким образом, теорема 6.1 верна и для завершённой Е-схемы модели. 6.2. Завершаемость второй части алгоритма Вторая часть алгоритма (3) состоит в выполнении процедуры фильтрования завершённой схемы модели. Выполнение этой процедуры состоит из проверок подтверждения обещаний в основных вершинах и выполнении процедур ±-разметки. Вторая теорема о завершаемое работы алгоритма будет следовать из доказательства конечности числа шагов в процедуре фильтрования. Лемма 6.10. Проверка подтвержденности обещания в в вершине СІ выполняется за конечное число шагов. Доказательство. Число основных цепей и число основных а.п. в силу леммы 6.3 и отсутствия в G кратных дуг конечно. В силу конечности числа вершин в основных цепях и основных а.п. проверка подтвержденности обещания в каждой основной цепи и основном а.п. проводится за конечное число шагов. Поэтому и проверка подтвержденности обещания в в вершине СІ выполняется за конечное число шагов. Лемма доказана.
Похожие диссертации на Алгоритм распознавания выполнимости формул логики ветвящегося времени и его применение
