Метод резолюций проверки общезначимости и противоречивости формул логики высказываний, применение метода для Хорновских дизъюнктов

Примеры:

1)     -

      Res( )=

2) -

      Res( )=

Определение пустой резольвенты:

      Резольвента двух дизъюнктов и называется простой и обозначается

Теорема 1. Пусть элементарные дизъюнкты и имеют вид:

, . Тогда резольвента есть логическое следствие дизъюнктов и и

.                                                                    (1)

Доказательство. Формулы и равносильны тогда и только тогда, когда составная формула

                                                                       (2)

является  законом логики. Построим таблицу истинности для этой формулы: 

 

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

что и требовалось  доказать. ■ 

Применим эту теорему к проверке общезначимости формулы . Построим вначале отрицание и приведем полученную формулу к КНФ. Получим так называемую клаузальную форму (в логике высказываний она всегда совпадает с КНФ).

,

где - элементарные дизъюнкты.

Рассмотрим  цепочку равносильных формул:

   

         

Очевидно, что  резольвента является дизъюнктом. Обозначим символом , и снова попробуем образовать резольвенту каких-нибудь дизъюнктов. Если она нашлась, то получим еще одну равносильную формулу. И так далее.

     Ясно, что процесс, в конце концов, остановится, поскольку число различных дизъюнктов от переменных не превышает (мы считаем, что переменные в одном дизъюнкте не повторяются).

      После остановки процесса возможны 2 случая:

▪   получилась пустая резольвента, то есть на предыдущем шаге было получено противоречие:

   

 

      

для некоторой  логической переменной .

Поэтому формула  является противоречием, и формула - тавтология. Таким образом, справедлива теорема:

            Теорема 2: Если процесс  построения резольвент привёл построение пустой резольвенты, то  - противоречие, - тавтология.■ 

▪   больше не получается образовывать новых резольвент, отличных от уже полученных дизъюнктов.

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

     Доказательство:

   

.

Первой формуле  соответствует множество дизъюнктов ,  второй формуле соответствует множество дизъюнктов , где , и т.д. …..

     Предположим на некотором шаге получим формулу и множество дизъюнктов , из которых нельзя образовать новых резольвент. Ясно, что множество имеет вид:

      , и 

, 
 

где каждый дизъюнкт в первом подмножестве резольвирует с некоторым дизъюнктом из первого  подмножества (будем называть их дизъюнктами типа I), а дизъюнкты из второго подмножества не резольвируют с другими дизъюнктами в . Дизъюнкты из первого подмножества будем называть дизъюнктами I типа, дизъюнкты из второго – дизъюнктами II типа.  

      Если  переменная входит в дизъюнкт II типа без отрицания, то она может входить в другие дизъюнкты II типа тоже только без знака отрицания. Если входит в , то во все остальные дизъюнкты II типа переменная может входить только со знаком отрицания.

      Придадим  значение 1 всем переменным, входящим без  отрицания в дизъюнкты в  . Придадим значение 0 всем переменным, входящим со знаком отрицания в . На построенном наборе значений переменных, дизъюнкты будут дизъюнктивной суммой единичных слагаемых и сами примут логическое значение 1.  

      Всем  переменным, не входящим в дизъюнкты  , присвоим произвольное логическое значение.

      Рассмотрим  логическое значение формулы 

на построенном  наборе значений переменных. Каждый дизъюнкт I типа, очевидно, содержит дизъюнктивное слагаемое, содержащееся в некотором дизъюнкте II типа. Это слагаемое имеет значение 1 на выбранном наборе значений переменных. Значит, все дизъюнкты имеют логическое значение 1. Поэтому формула имеет на этом наборе логическое значение 1 и не является противоречием. Значит, формула не является тавтологией.   ■  
 
 
 
 
 
 
 

     Алгоритм  метода резолюций

1. Построить
2. Привести  к КНФ
3. Построить множество дизъюнктов ⧍
4. Провести анализ пар из множества ⧍. Если существует дизъюнкт содержащий переменную P и существует  содержащий , то соединяем эти дизъюнкты при помощи , убирая при том P и

     Получаем  новый дизъюнкт (резольвенту)

5. Если получилась пустая резольвента, то Ф – тавтология. Конец алгоритма (выход)

 

     Если  резольвента не пустая и отлична  от элементов множества ⧍, то добавляем её ко множеству ⧍ и переходим к шагу 4.

     Если  не получилось добавить новые резольвенты к ⧍, то Ф не является тавтологией

     Конец алгоритма (выход) 
 

3. Недостатки  метода резолюций и его эффективность  в случае произвольного множества дизъюнктов.

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

5. Применение  метода резолюций для Хорновских  дизъюнктов. 

Определение Хорновских дизъюнктов:

      Дизъюнкт  называется хорновским, если он содержит не более одной переменной без отрицания

Примеры хорновских и не хорновских дизъюнктов:

- хорновский дизъюнкт

- не хорновский дизъюнкт 

Суть метода резолюций в этом случае заключается

      В получении противоречивого выражения  в формуле Ф. Если Ф будет противоречиво, то формула будет являться тавтологией.

Определение выполнимого/невыполнимого, противоречивого/непротиворечивого  множества дизъюнктов:

1. Множество дизъюнктов формулы Ф является противоречивым, когда при сопоставлении дизъюнктов мы получим пустую резольвенту, иначе множество дизъюнктов Ф будет являться непротиворечивым.
2. Множество дизъюнктов формулы Ф является выполнимым, когда формула Ф будет являться тавтологией, иначе множество дизъюнктов Ф невыполнимо.

 

Решение задач. 

1. Проверить на противоречивость множество хорновских дизъюнктов

Ф-{A B C D,B, A B C,C, B D} 

 

     Множество Ф противоречиво. 

     2.Проверить  на противоречивость множество  дизъюнктов 

   Ф={P ,Q,R,T R,T , }