Метод резолюций проверки общезначимости и противоречивости формул логики высказываний, применение метода для Хорновских дизъюнктов
Курсовая работа, 05 Января 2012, автор: пользователь скрыл имя
Описание работы
Рассмотрим метод резолюций в логике высказываний, затем проверим формулы на общезначимость и противоречивость. Так же рассмотрим применение метода Хорно.
Цель работы:
Научиться использовать метод резолюций для проверки формул. Доказать является ли формула тавтологией, при помощи метода резолюций. Применение метода резолюции с хорновским дизъюнктом.
Работа содержит 1 файл
1 вариант.doc
— 559.00 Кб (Скачать)| Номер шага | P |
Q | R | T |
T |
|
| 1 | P |
Q | R | T |
T | |
| 2 | P |
Q | R | T |
T | |
| 3 | P | Q | R | T |
T | |
| 4 |
На
шаге 4 получаем 0, являющийся резолютивным
выводом из S. Следовательно, множество
Ф противоречиво.
- Заключение
- Разобрали определения, встречающиеся в работе
- Рассмотрели метод резолюций для проверки формул на общезначимость, способ проверки на противоречивость при помощи хорновских дизъюнктов.
- Разобрали на примере способ проверки на противоречивость при помощи хорновских дизъюнктов
- Список литературы
- Судоплатов С.В., Овчинников Е.В., «Математическая логика и теория алгоритмов», М, Инфра-М, 2005
- Э.Мендельсон «Введение в математическую логику»: пер. с англ., М.: изд-во Наука, 1971.
- А.К. Гуц «Математическая логика и теория алгоритмов»
- Ю.П. Кораблин «Основы математической логики»