7 - Метод резолюций. Скулемовские функции. Метод резолюций для исчисления высказываний. Метод резолюций для исчисления предикатов (Конспект лекций), страница 2

А проверку формулы на противоречивость можно провести, используя ее скулемовскуюстандартную форму, в которой не используется импликация, а отрицания относятся непосредственно к атомам формулы.Подобный подход привел к разработке метода, известного как метод резолюций. Использование этого метода начнем с алгебры высказываний.Рассмотрим некоторое множество Γ дизъюнктов. Мы можем считать, что в каждом дизъюнкте литера с данной переменной x входит только один раз, поскольку дизъюнкция одинаковых литер есть сама эта литера, а дизъюнкция контрарных литер (т.е. одна являетсяотрицанием другой) дает дизъюнкт, являющийся тавтологией.

Такой дизъюнкт не влияет напротиворечивость всего множества и его можно из рассмотрения убрать.ÔÍ-12ÔÍ-127.2. Метод резолюций для исчисления высказыванийÌÃÒÓe 1 , D2 = ¬p ∨ De 2 . Нам нужно убедиться в истинности формулы D1 ∧ D2 →J Пусть D1 = p ∨ De 1, De 2 .

Подставимe1 ∨ De 2 ), что равносильно выводимости генценовской секвенции D1 , D2 > D(De 1 , ¬p ∨ De2 > De 1, De 2 . Имеем:в эту секвенцию представление дизъюнктов D1 и D2 : p ∨ De 1 , ¬p ∨ De2 > De 1, De2p∨De2 > De 1, De2p, ¬p ∨ De2 > De 1, De2p, De 1, De 2, pp, > De 1 , ¬p ∨ De2 > De 1, De 2 выводима в генценовском исчислении. СледоИтак, секвенция p ∨ Doneeвательно, множество из одного дизъюнкта D1 ∨ D2 есть логическое следствие множествадизъюнктов {D1 , D2 }.

IÔÍ-12ÌÃÒÓÔÍ-12Доказанная теорема приводит к следующей процедуре обоснования противоречивости множества дизъюнктов. Отталкиваясь от исходного множества S0 , находим контрарную пару,конструируем ее резольвенту и добавляем к S0 , получая S1 . С множеством S1 поступаем аналогично, пропуская, правда, уже рассмотренную контрарную пару.

Для автоматизации процессаможно предложить следующий алгоритм. Множество рассматриваем как упорядоченный список, резольвенты добавляем в конец списка, а текущее состояние всего списка фиксируем паройиндексов — номер рассматриваемой пары в списке. Завершением этой процедуры являетсяполучение пустого дизъюнкта, что и является доказательством противоречивости исходногомножества.Действительно, каждая вновь получаемая резольвента есть логическое следствие текущегомножества Si дизъюнктов. Значит, ее добавление к множеству дает новое множество, котороес точки зрения противоречивости эквивалентно исходному.

Если на очередном шаге возникаетпустой дизъюнкт, то последнее множество дизъюнктов противоречиво, а значит, противоречивои исходное множество дизъюнктов. В этом и состоит суть метода резолюций.Поскольку возникающий пустой дизъюнкт есть резольвента двух уже имеющихся дизъюнктов, которые в свою очередь есть либо дизъюнкты исходного множества, либо резольвенты.Возникает дерево, отражающее процесс построения пустого дизъюнкта из имеющегося множества дизъюнктов.

Это приводит к следующему определению.Последовательность дизъюнктов, в которой каждый дизъюнкт либо принадлежит множеству Γ, либо является резольвентой двух предыдущих дизъюнктов, называется резолютивным выводом из множества Γ. Конечный дизъюнкт резолютивного вывода из множестваΓ называется выводимым из множества Γ.ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÌÃÒÓe 1 , ¬p ∨ De2 > De 1, De2DÌÃÒÓÔÍ-12Теорема 7.2. Пусть дизъюнкты D1 и D2 образуют контрарную пару. Тогда их резольвентаявляется логическим следствием множества дизъюнктов {D1 , D2 }.ÔÍ-12ÔÍ-12ÌÃÒÓ73ÌÃÒÓÌÃÒÓÔÍ-12Предположитм, что Γ = {D1 , D2 , . . . , Dk }, причем дизъюнкт D1 содержит переменную p, аe 1 , D2 = ¬p∨ De 2 , где De1 и De 2 не содержат переменной p.дизъюнкт D2 — литеру ¬p, т.е. D1 = p∨ DТакие дизъюнкты будем называть контрарной парой.

Тогда можно рассмотреть дизъюнктe1 ∨ De 2 вообще не содержащий переменной p. Этот дизъюнкт называется резольвентойDдизъюнктов D1 , D2 .Введем очевидное понятие: формула B называется логическим следствием формулы A, еслиформула A→B является тавтологией. В исчислении высказываний (и в исчислении предикатовтоже) это равносильно существованию выводимости A ` B или выводимости секвенции A >B.

Множество дизъюнктов ∆ назовем логическим следствием множества дизъюнктов Γ, есликонъюнкция всех дизъюнктов ∆ есть логическое следствие конъюнкции всех дизъюнктов Γ.e 1, De2p, ¬p > DÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓ7. Метод резолюцийÔÍ-12ÌÃÒÓN11x2N12x2N21x2N22x3x3x2N23x3x3N24x3x3x3Рис. 7.1ÔÍ-12Листьям этого бинарного дерева соответствуют конкретные наборы значений переменных. Поусловию при каждом таком наборе значений один из дизъюнктов противоречив, поскольку конъюнкция всех дизъюнктов является противоречием. Рассмотрим пару листьев, выходящих изодного узла: L1 с xn = 0 и L2 с xn = 1. Пусть им соответствуют дизъюнкты D1 и D2 .

Возможны два варианта. В первом варианте один из дизъюнктов, например D1 , противоречив дляe 1 ∨ xσn , тообоих листьев. Тогда D1 не содержит переменной xn . Действительно, если D1 = Dпри xn = σ, т.е. для одного из двух листов, дизъюнкт D1 будет истинным. В этом вариантеудаляем два листа, а дизъюнкт D1 приписываем узлу, порождающему листы L1 и L2 . Послеудаления листьев, порождающих их узедл станет листом.Во втором варианте дизъюнкт D1 противоречив в листе L1 (т.е.

при xn = 0) и истинненв листе L2 , а дизъюнкт D2 противоречив в листе L2 и истиннен в L1 . Тогда D1 имеет видÌÃÒÓ. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .ÃÒÓÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12x1ÔÍ-12N0x1ÌÃÒÓJ В примере фактически уже было доказано, что если существует вывод пустого дизъюнкта, то исходное множество дизъюнктов противоречиво. Чтобы доказать противоположноеутверждение, рассмотрим некоторое противоречивое множество дизъюнктов Γ. Добавляя кнему последовательно резольвенты различных контрарных пар, получаем расширение исходного множества с сохранением его противоречивости.

Это расширение потихоньку поглощаетдерево вывода пустого дизъюнкта, существование которого необходимо доказать. Что можетбыть мерой близости к пустому дизъюнкту? Например, количество литер в очередной резольвенте. Чем короче очередной получаемый дизъюнкт, тем ближе дизъюнкт нулевой доины, т.е.пустой.Процедуру перехода ко все более коротким дизъюнктам можно описать геометрически.

Всепеременные, встречающиеся в исходном списке дизъюнктов Γ, расположим в виде последовательности: x1 , x2 , . . . , xk . Перебор всех вариантов значений этих переменных можно представить в виде дерева, в котором метка дуги xi означает, что xi = 1 (истинно), а метка ¬xi — чтоxi = 0 (ложно) (рис. 7.1).ÔÍ-12Теорема 7.3. Множество Γ дизъюнктов противоречиво тогда и только тогда, когда существует вывод из этого множества пустого дизъюнкта.ÌÃÒÓÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ИУ-9, МЛТА, 2009-10уч.г.Пример 7.3. Рассмотрим множество Γ = {¬x ∨ y, ¬y, x}. Тогда резолютивным выводомдля этого множества является следующий:• ¬x ∨ y — дизъюнкт множества Γ;• x — дизъюнкт множества Γ;• y — резольвента двух предыдущих;• ¬y — дизъюнкт множества Γ;• — резольвента двух предыдущих.Отметим, что получение пустого дизъюнкта как результата вывода означает, что исходноемножество дизъюнктов Γ противоречиво.

Действительно, последовательно добавляя к Γ формулы из вывода, получаем последовательность расширяющихся множеств дизъюнктов, в которойкаждое очередное множество есть логическое следствие предыдущего. Последнее множествосодержит пустой дизъюнкт и, следовательно, является противоречивым. Поэтому и исходноемножество дизъюнктов является противоречивым.x3ÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓ74ÌÃÒÓ12nϑ1 ◦ ϑ2 =x1t1 ϑ 2x2t2 ϑ 2......xntn ϑ2y1q1y2q2......ynqnÔÍ-12(запись ti ϑ2 означает, что в терме ti надо выполнить подстановку ϑ2 ).

Ясно, что композиция подстановок реализует последовательное применение двух подстановок к формуле, причемпоследовательность применения — слева направо.Унификатор ϑ множества формул Φ1 , Φ2 ,. . . , Φk называется наиболее общим, если любойунификатор λ этого множества можно представить в виде λ = ϑ ◦ σ с помощью некоторойподстановки σ.Унификация — процедура, позволяющая (при некоторых условиях) сохранять свойство противоречивости, но при этом согласовывать аргументы у одинаковых предикатных символов.ÌÃÒÓПример 7.5. Множество из формул p(a, y); p(b, f (x)) не имеет унификаторов, поскольку любая подстановка меняет переменные, но не константы.

Следовательно, при любой подстановкеϑ первая формула будет иметь вид p(a, T1 ), а вторая p(b, T2 ), где T1 и T2 — некторые термы соответствующего сорта. Значит, никакая подстановка не приведет к тому, что формулы станутодинаковыми.Подстановки можно применять последовательно. Пусть есть подстановки ϑ1 = xt 1 xt 2 .. ..

.. xt n1 2ny1 y2 . . . ynи ϑ2 = q q . . . q . Их композицией ϑ1 ◦ ϑ2 называется подстановкаÔÍ-12оно унифицируемо.ÌÃÒÓÔÍ-12ÌÃÒÓВ случае исчисления предикатов резолютивный вывод касается бескванторных формул, нопод литерой дизъюнкта надо понимать элементарную формулу, в которую в качестве аргументов предикатного символа могут входить различные термы. Это усложняет ситуацию,поскольку один предикатный символ в зависимости от комбинации термов в его аргументахможет давать разные истинностные значения. Но правило резолюций остается тем же: еслиесть дизъюнкты P ∨ D1 и ¬P ∨ D2 , то их заменяем резольвентой D1 ∨ D2 .