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

Автор: Пользователь скрыл имя, 05 Января 2012 в 16:02, курсовая работа

Описание работы

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

Работа содержит 1 файл

1 вариант.doc

— 559.00 Кб (Скачать)
Номер шага P
Q R T
R
T
1 P
Q R T
R
T
2 P
Q R T
R
T
3 P Q R T
R
T
4          
 

         На  шаге 4 получаем 0, являющийся резолютивным выводом из S. Следовательно, множество Ф противоречиво. 

  1. Заключение
    1. Разобрали определения, встречающиеся в работе
    1. Рассмотрели метод резолюций для проверки формул на общезначимость, способ проверки на противоречивость при помощи хорновских дизъюнктов.
    2. Разобрали на примере способ проверки на противоречивость при помощи хорновских дизъюнктов
 
  1. Список  литературы
    1. Судоплатов С.В., Овчинников Е.В., «Математическая логика и теория алгоритмов», М, Инфра-М, 2005
    1. Э.Мендельсон «Введение в математическую логику»: пер. с англ., М.: изд-во Наука, 1971.
    2. А.К. Гуц  «Математическая логика и теория алгоритмов»
    3. Ю.П. Кораблин «Основы математической логики»

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