Метод резолюций и его применение в алгебре высказываний и алгебре предикатов

, F₂ равносильна (Y Z).

Тогда множество дизъюнктов S равно {X, , Y Z, }.

Из множества S легко выводится  пустой дизъюнкт: , , , Y Z, Y, □.

Следовательно, формула G является логическим следствием формул F₁, и F₂.

Общезначимость правила  резолюций выражается следующей  леммой.

Лемма (1). Пусть s₁ и s₂ – дизъюнкты нормальной формы S, l – литера. Если

 и  ,то дизъюнкт  является логическим

следствием нормальной формы S. (Дизъюнкт r называется резольвентой дизъюнктов s₁ и s₂).

Следствие. Нормальные формы S и S эквивалентны.

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

Доказательства  невыполнимости, основанные на принципе резолюций.

Доказательства невыполнимости логических формул очень важны в  ИИ (Искусственный Интеллект). Способы  таких доказательств, основанные на принципе резолюций, выделяются среди прочих тем, что они дают возможность использовать средства автоматического доказательства, применяемые в логическом программировании.

При всей простоте метод  резолюций (или, короче, резолюция) достаточен для обнаружения возможной невыполнимости множества приведённых дизъюнктов. Таким образом, можно попробовать доказать невыполнимость конечного множества дизъюнктов из S с помощью следующего алгоритма.

При условии, что □  S:

1)выбираем l, s₁ и s₂, такие что и ;

2) вычисляем резольвенту r;

3) заменяем S на S .

В качестве примера проверим невыполнимость множества S= .

Дизъюнкты удобно пронумеровать, получится следующий список:

1.

2.

3.

4.

Затем вычисляются и добавляются  к S резольвенты. В списке, который приводится ниже, каждый дизъюнкт – резольвента некоторых из предшествующих дизъюнктов. Номера их приведены в скобках справа от соответствующей резольвенты.

5.      (1,3)

6.           (1,4)    

7.      (2,3)

8.            (2,4)

9.           (2,5)

10.          (3,6)

11.         (3,8)

12.           (4,5)

13.          (4,7)

14.  □        (4,9)

Замечание. Алгоритм проверки невыполнимости – недетерминированный, вообще говоря, возможен не один выбор для l, s₁ и s_2. В приведённом примере мы выбирали дизъюнкты s₁ и s₂  в лексикографическом порядке номеров. Такая стратегия неоптимальна. Некоторые резольвенты оказались ненужными, а также вычислялись в некоторых случаях более одного раза. Для сравнения продемонстрируем теперь применение этого же алгоритма с минимумом резолюций:

5.      (1,4)

6.       (2,4)

7.       (3,6)

8. □      (5,7)

Ясно, что принятая стратегия  может значительно влиять на процесс  выполнения алгоритма. Тем не менее  упомянем два важных свойства, не зависящих  от используемой стратегии.

Прежде всего, если множество S не содержит ни одной пары дизъюнктов, допускающих резольвенту, то оно выполнимо (разумеется, за исключением случая, когда оно содержит пустой дизъюнкт). Интерпретация I получается заданием l(p)=И тогда и только тогда, когда положительная литера p принадлежит одному из дизъюнктов множества S.

Во-вторых, если выполнение этого алгоритма закончилось  «нормально» после порождения пустого  дизъюнкта, то установлена невыполнимость исходного множества S. Это непосредственное следствие леммы 1.

Может случиться, что  выполнение алгоритма не завершится, хотя число различных дизъюнктов, которые могут быть порождены  с помощью резолюций, очевидно, конечно. Например, такое явление имеет  место для множества  . Резольвентный дизъюнкт q будет порождаться неограниченное число раз. Рассмотрим также случай невыполнимого множества . Оптимальная стратегия установит невыполнимость посредством построения резольвент q, а затем □. Напротив, «неадекватная» стратегия приведёт к зацикливанию, которое только что  было отмечено. Таким образом, можно констатировать, что стратегия влияет не только на эффективность алгоритма, но и на его завершаемость.

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

  Лемма (2). Если множество дизъюнктов S невыполнимо и содержит резольвенты своих элементов, то оно обязательно содержит пустой дизъюнкт.

Число различных дизъюнктов, которые можно составить на основе конечного множества S, конечно. Таким образом, лемма 2 лаёт простое общее средство решения вопроса о выполнимости или невыполнимости конечного множества дизъюнктов.

Проиллюстрируем лемму  одним очень простым примером. Рассмотрим множество дизъюнктов S= .  Первый этап состоит в построении семантического дерева и помечивании каждого листа дизъюнктом, делающим ложной интерпретацию, соответствующую этому листу. Это возможно тогда и только тогда, когда S невыполнимо. Здесь именно такой случай и подходящее дерево изображено на рисунке 1.

 

Рис.1.

Второй этап состоит  в том, что каждому узлу N дерева сопоставляется некоторый дизъюнкт с. Этот дизъюнкт будет зависеть од дизъюнктов с₁ и с_2, которые уже сопоставлены двум узлам, следующим за N. Две соответствующие дуги помечены двумя противоположными литерами, скажем и . Если один из дизъюнктов, например с₁  не содержит ни , ни её отрицание, то можно выбрать с= с₁, в противном случае с будет резольвентой для с₁ и с₂   по отношению к   . Этот результат, полученный для множества S, иллюстрируется рисунком 2.

 

Рис.2.

Заметим, что каждый узел помечен дизъюнктом, при котором ложна частичная интерпретация, соответствующая этому узлу. Таким образом, корень будет помечен пустым дизъюнктом. Наконец, по построению каждый дизъюнкт является элементом S или получен из S с помощью резолюции. Число резольвент, которые надо вычислить для установления невыполнимости множества дизъюнктов S, не больше числа невисячих узлов семантического дерева. Максимальное значение этой величины равно , где n-число различных высказываний, входящих в S. Тем самым показано, что резолюция неэффективна, если применяется только что описанная простая стратегия. Отметим, что некоторые стратегии выбора приводят к лучшим реализациям.

Лемма 2 остаётся справедливой для бесконечного S. Отсюда следует, что бесконечное множество дизъюнктов невыполнимо тогда и только тогда, когда в нём найдётся конечное невыполнимое подмножество. Приведём непосредственное следствие, отражающее свойство завершаемости принципа резолюции.

Следствие. Если множество S формул невыполнимо, то этот факт всегда можно установить методом резолюций.

 

 

 

 

 

 

 

 

 

 

 

 

 

 

Приложения  и примеры использования метода резолюций.

Метод резолюций применяется  в качестве механизма доказательства при реализации принципа дедукции: формула С является логическим следствием конечного множества Е тогда и только тогда, когда невыполнимо.

Резолюция – ещё и  такой механизм, который служит основой  для осуществления инструкций на языке Пролог.

В качестве примера установим Общезначимость одного расхожего метода доказательства, называемого доказательством разбором случаев. Обозначим гипотезу через h, где возможны два случая – через p и q, а заключение – через c. Требуется доказать: . Это сводится к доказательству невыполнимости множества . Тогда множество дизъюнктов, невыполнимость которого следует установить, таково: .

Исходя из этого множества, можно  следующим образом получить пустой дизъюнкт:

1.                гипотеза

2.      гипотеза

3.           гипотеза

4.           гипотеза

5.               отрицание заключения

6.           резольвента для 1 и 2

7.                резольвента для 3 и 5

8.                резольвента для 4 и 5

9.                резольвента для 6 и 7

10. □            резольвента для 8 и 9

Всякое доказательство, формальное или неформальное, является последовательностью элементарных рассуждений, последнее из которых и есть заключение (в данном случае это □, потому что речь идёт об опровержении. Однако взаимосвязь между различными этапами доказательства, есть не что иное, как отношение частичного порядка. Таким образом, естественно, хотя менее удобно, представлять доказательство деревом, а не последовательностью. В случае доказательства с помощью метода резолюций это дерево будет семантическим. Дерево нашего примера изображено на рисунке 3 (узлы помечены номерами дизъюнктов, а не самим дизъюнктами).

Рис. 3.

Правило согласия (в оригинале  – consensus(лат.)) двойственно правилу резолюций. Если его применить к конъюнкциям и , то получим конъюнкцию . Эта операция была введена в рамках булевой алгебры применительно к синтезу логических схем. Она позволяет выявлять Общезначимость ДНФ (Дизъюнктивной Нормальной Формы).

 

 

 

Метод резолюций  в логике предикатов.

В процедуре доказательства по методу резолюций для того, чтобы  отождествлять контрарные пары литер, мы очень часто должны унифицировать (склеивать) два или более выражения, то есть мы должны находить подстановку, которая может сделать несколько выражений тождественными. Итак, рассмотрим унификацию выражений.

Подстановка называется унификатором для множества тогда и только тогда, когда = =…= . Говорят, что множество унифицируемо, если для него существует унификатор. Унификатор для множества выражений будет наиболее общим унификатором тогда и только тогда, когда для каждого унификатора для этого множества существует такая подстановка , что = .

Например, множество  унифицируемо, так как подстановка является его унификатором.

Рассмотрим алгоритм унификации для  нахождения наиболее общего унификатора  для конечного унифицируемого множества  непустых выражений. Когда множество  не унифицируемо, алгоритм будет выявлять также и этот факт.

Пусть даны и . Эти два множества не тождественны. Рассогласование в том, что встречается в , а переменная в . Чтобы отождествить и , мы сперва должны найти рассогласование, а затем попытаться его исключить. Для и рассогласование будет . Так как - переменная, то можно заменить на , и таким образом рассогласование будет исключено. В это и заключается идея, на которой и основан алгоритм унификации.

Множество рассогласований  непустого множества выражений  получается выявлением первой (слева) позиции, на которой не для всех выражений из стоит один и тот же символ и затем выписыванием из каждого выражения в подвыражения, которое начинается с символа, занимающего эту позицию. Множество этих подвыражений и есть множество рассогласований в .

Например, если есть , то первая позиция, в которой не все выражения из состоят из одинаковых символов, есть пятая, так как все выражения имеют одинаковые первые четыре символа ( . Таким образом, множество рассогласований состоит из соответствующих подвыражений, которые начинаются с пятой позиции , и это в действительности множество .

Алгоритм унификации.

Шаг 1. Множество  и .

Шаг 2. Если - единичный дизъюнкт, то остановка - наиболее общий унификатор для . В противном случае найдём множество рассогласований для .

Шаг 3. Если существуют такие элементы и в , что - переменная, не входящая в , то перейти к шагу 4. В противном случае остановка: не унифицируемо.

Шаг 4. Пусть  и . (Заметим, что = .)

Шаг  5. Присвоить значение и перейти к шагу 2.

Пример 1.  Найти наиболее общий унификатор для

1. и . Так как - не единичный дизъюнкт, то не является наиболее общим унификатором для .

2. Множество рассогласований . В существует переменная , которая не встречается в .

3. Пусть 

=