Автор: Пользователь скрыл имя, 05 Января 2012 в 16:02, курсовая работа
Рассмотрим метод резолюций в логике высказываний, затем проверим формулы на общезначимость и противоречивость. Так же рассмотрим применение метода Хорно.
Цель работы:
Научиться использовать метод резолюций для проверки формул. Доказать является ли формула тавтологией, при помощи метода резолюций. Применение метода резолюции с хорновским дизъюнктом.
РОССИЙСКИЙ
ГОСУДАРСТВЕННЫЙ СОЦИАЛЬНЫЙ УНИВЕРСИТЕТ
Факультет информационных
технологий
Курсовая Работа
по математической
логике
«Метод резолюций
проверки общезначимости и противоречивости
формул логики высказываний, применение
метода для Хорновских дизъюнктов»
Выполнил:
Студент группы ИВТ-ДБ-2
Поздняков А.В.
Проверила:
Доцент Маренич
В.Е.
2011
г. Москва
Рассмотрим
метод резолюций в логике высказываний,
затем проверим формулы на общезначимость
и противоречивость. Так же рассмотрим
применение метода Хорно.
Цель работы:
Научиться использовать метод резолюций для проверки формул. Доказать является ли формула тавтологией, при помощи метода резолюций. Применение метода резолюции с хорновским дизъюнктом.
Высказыванием называется любое предположение, о котором можно сказать истинно оно или ложно.
Примеры:
Каир-столица Египта
Луна – спутник земли.
Заметим, что не всякое предположение является высказыванием.
Примеры:
Скоро откроется каток.
Ночью
на улице будет холодно.
Отрицание
высказывания А - это новое высказывание,
которое обозначается
и которое ложно, когда А истинно и
истинно, когда А ложно.
Дизъюнкция двух высказываний - это новое высказывание, обозначаемое , которое:
ложно, если А и В – ложные высказывания, и истинно во всех других случаях.
A | B | |
1 | 1 | 1 |
1 | 0 | 1 |
0 | 1 | 1 |
0 | 0 | 0 |
Конъюнкция двух высказываний - это новое высказывание, обозначаемое , которое:
истинно, если А и В – истинные высказывания, и ложно в остальных случаях.
A | B | |
1 | 1 | 1 |
1 | 0 | 0 |
0 | 1 | 0 |
0 | 0 | 0 |
Определение формулы логики высказываний:
Формула логики высказываний – называется такая формула, которая удовлетворяет условиям:
Порядок выполнения операций в файле задаётся скобками. Количество скобок можно уменьшить, если ввести приоритеты операций
Примеры:
1) ;
2) .
Формула, содержащая переменную обозначается, как Ф( )
Если
вместо переменных
подставить высказывание
, то получим составное
высказывание.
Тавтологией называется формула логики высказываний, которая принимает значение 1 («истинно») при любых значениях входящих в неё переменных.
Примеры:
1. Для
данных высказываний
если
”Каждый студент нашего вуза - отличник”
1) - истинное высказывание
2) - ложное высказывание
3) - истинное высказывание
4) и - истинное высказывание
5) - ложное высказывание
6) или , то каждый студент нашего вуза – отличник – истинное высказывание
7) ( ) - истинное
1 1
8) - ложное высказывание
1 1 0 0 0
1______
1
0__
2. Является ли следующая формула законом логики (тавтологией)
|
||||||
1 | 1 | 0 | 0 | 1 | 1 | 1 |
1 | 0 | 0 | 1 | 0 | 0 | 1 |
0 | 1 | 1 | 0 | 1 | 1 | 1 |
0 | 0 | 1 | 1 | 1 | 1 | 1 |
Формула
принимает значение 1 (истина) при
любых значениях входящих в неё переменных.
Поэтому по определению формула является
тождественно истинной.
Противоречием
логики высказываний
называется формула, которая принимает
значение 0 («ложь») при любых значениях
входящих в неё переменных.
Определение равносильности формул. Две формулы и называются равносильными, пишем , если они принимают одинаковое значение при одинаковых наборах переменных.
Ясно, что две формулы
и
равносильны тогда и только тогда,
когда «составная» формула
является законом логики высказываний.
Определение элементарной дизъюнкции и конъюнкции
1) Элементарной дизъюнкцией (дизъюнктом) называется выражение вида , где - логическая переменная или её отрицание (для )
2) Элементарной конъюнкцией
(конъюнктом) называется выражение вида
, где
- логическая переменная
или её отрицание
(для
)
Примеры:
1)
2)
Определение ДНФ, КНФ для данной формулы Ф
А)
Б)
имеет вид
, где
- элементарный конъюнкт (
)
А)
Б)
имеет вид
, где
- элементарный
дизъюнкт (
)
Примеры
- ДНФ из 3-х конъюнктов
- ДНФ из 1-ого конъюнкта
Пусть формула Ф( ) является тавтологией
- тавтология, значит - ДНФ
- ДНФ
Пусть формула Ф( ) является тавтологией
- тавтология, значит - КНФ для 1ого дизъюнкта
- КНФ
- ДНФ из 1ого конъюнкта
- КНФ
Определение СДНФ:
СДНФ называется такая ДНФ, в которой каждая элементарная конъюнкция содержит все логические переменные или их отрицания ( ) по одному разу.
Определение СКНФ:
СКНФ называется такая КНФ, в которой каждая элементарная дизъюнкция содержит все логические переменные или их отрицания ( ) по одному разу. Элементарные дизъюнкции в СКНФ не повторяются
Каждая
логика высказываний, кроме противоречия,
имеет единственную СДНФ. Противоречие
СКНФ не имеет
3.
Метод резолюций
Метод резолю́ций
– это правило вывода, восходящее
к методу доказательства теорем через
поиск противоречий; используется в логике
высказываний и логике предикатов первого
порядка. Правило резолюций, применяемое
последовательно для списка резольвент,
позволяет ответить на вопрос, существует
ли в исходном множестве логических выражений
противоречие.
Основа
метода резолюций была предложена в
1930 году в докторской
диссертации Эрбрана для доказательства
теорем в формальных системах первого
порядка. На ЭВМ метод резолюций был
впервые реализован Джоном
Аланом Робинсоном в
1965г.
Мы рассмотрим метод резолюций в логике высказываний.
Пусть дана формула Ф. Является ли она тавтологией?
Для ответа
на этот вопрос используется метод
резолюций.
В основе метода резолюций лежат теоремы 1, 2, 3, приведенные ниже.
Введем вначале понятие резольвенты двух дизъюнктов.
Определение (резольвенты).
Резольвентой дизъюнктов вида и называется дизъюнкт res( )= , где - дизъюнкты, - переменные.