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

РОССИЙСКИЙ  ГОСУДАРСТВЕННЫЙ СОЦИАЛЬНЫЙ УНИВЕРСИТЕТ 
 

Факультет информационных технологий 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Курсовая  Работа

по математической логике 
 

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

Выполнил:

Студент группы ИВТ-ДБ-2

Поздняков А.В.

Проверила:

Доцент Маренич В.Е. 
 
 

2011

г. Москва

1. Введение

      Рассмотрим  метод резолюций в логике высказываний, затем проверим формулы на общезначимость и противоречивость. Так же рассмотрим применение метода Хорно. 

Цель  работы:

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

 

2. Определение основных понятий

 

     Высказыванием называется любое предположение, о котором можно сказать истинно оно или ложно.

     Примеры:

     Каир-столица  Египта

     Луна  – спутник земли.

      Заметим, что не всякое предположение является высказыванием.

      Примеры:

      Скоро откроется каток.

      Ночью на улице будет холодно. 

1. Определение не является высказыванием.
2. Не всякое предположение является высказыванием.

 

     Отрицание высказывания А -  это новое высказывание, которое обозначается и которое ложно, когда А истинно и истинно, когда А ложно. 

      Дизъюнкция двух высказываний - это новое высказывание, обозначаемое , которое:

ложно, если А и В – ложные высказывания, и истинно во всех других случаях.

 
 
 
 
 

      Конъюнкция двух высказываний  - это новое высказывание, обозначаемое , которое:

истинно, если А и В – истинные высказывания, и ложно в остальных случаях.

 
 

Определение  формулы логики высказываний:

Формула логики высказываний – называется такая формула, которая  удовлетворяет условиям:

1. Любая логическая переменная есть формула;
2. Если - формулы, то - тоже формулы;
3. Только те формулы являются формулами алгебры логики, которые удовлетворяют условию (1) и (2)

Порядок выполнения операций в файле  задаётся скобками. Количество скобок можно уменьшить, если ввести приоритеты операций

 

Примеры:

1) ;

2) .

      Формула, содержащая переменную обозначается, как Ф( )

      Если  вместо переменных подставить высказывание , то получим составное высказывание.  

     Тавтологией  называется формула логики высказываний, которая принимает значение 1 («истинно») при любых значениях входящих в неё переменных.

       Примеры:

     1. Для  данных высказываний определить  истинность высказываний определить истинность высказываний:

       если

          

           ”Каждый студент нашего вуза - отличник”

     1) - истинное высказывание

     2) - ложное высказывание

     3) - истинное высказывание

     4) и - истинное высказывание

     5) - ложное высказывание

     6) или , то каждый студент нашего вуза – отличник – истинное высказывание

     7) ( ) - истинное

                 1        1

     8) - ложное высказывание

                    1      1      0         0       0

                  1______           

                        1                     0__     

     2. Является  ли следующая формула законом  логики (тавтологией)

       

     Формула принимает значение 1 (истина) при  любых значениях входящих в неё переменных. Поэтому по определению формула является тождественно истинной. 

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

Определение равносильности формул. Две формулы и называются равносильными, пишем , если они принимают одинаковое значение при одинаковых наборах переменных.

  Ясно, что две формулы и равносильны тогда и только тогда, когда «составная» формула является законом логики высказываний. 

Определение элементарной дизъюнкции и конъюнкции

1) Элементарной дизъюнкцией (дизъюнктом) называется выражение вида , где - логическая переменная или её отрицание (для )

2) Элементарной конъюнкцией (конъюнктом) называется выражение вида , где - логическая переменная или её отрицание (для ) 

Примеры:

1)

2)  

   Определение ДНФ, КНФ для данной формулы Ф

1. ДНФ формулы F называется формула Ф такая, что:

А)

      Б) имеет вид , где - элементарный конъюнкт ( ) 

2.  КНФ формулы  F называется формула Ф такая, что:

А)

      Б) имеет вид , где - элементарный дизъюнкт ( ) 

   Примеры

1. - ДНФ из 2-х конъюнктов

- ДНФ из 3-х конъюнктов

  - ДНФ из 1-ого конъюнкта

2. - КНФ из 2-х дизъюнктов
3. ДНФ для тавтологии

Пусть формула  Ф( ) является тавтологией

- тавтология, значит - ДНФ

- ДНФ

4. КНФ для тавтологии

Пусть формула  Ф( ) является тавтологией

- тавтология, значит  - КНФ для 1ого дизъюнкта

- КНФ

5. ДНФ для Ф( ) – противоречие

- ДНФ из 1ого конъюнкта

6. КНФ для Ф( ) - противоречие

- КНФ 

Определение СДНФ:

     СДНФ  называется такая ДНФ, в которой  каждая элементарная конъюнкция содержит все логические переменные или их отрицания ( ) по одному разу.

Определение СКНФ:

      СКНФ  называется такая КНФ, в которой каждая элементарная дизъюнкция содержит все логические переменные или их отрицания ( ) по одному разу. Элементарные дизъюнкции в СКНФ не повторяются

      Каждая  логика высказываний, кроме противоречия, имеет единственную СДНФ. Противоречие СКНФ не имеет 

3.  Метод резолюций 

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

    Основа  метода резолюций была предложена в 1930 году в докторской диссертации Эрбрана для доказательства теорем в формальных системах первого порядка. На ЭВМ метод  резолюций был впервые реализован Джоном Аланом Робинсоном в 1965г.  
 

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

Пусть дана формула Ф. Является ли она тавтологией?

Для ответа на этот вопрос используется метод  резолюций. 

В основе метода резолюций лежат теоремы 1, 2, 3, приведенные ниже.

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

Определение (резольвенты).

      Резольвентой  дизъюнктов вида и называется дизъюнкт res( )= , где - дизъюнкты, - переменные.

Примеры:

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 , }