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

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

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

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

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

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

Выполнил:

Студент группы ИВТ-ДБ-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( )= , где - дизъюнкты, - переменные.