Студопедия

Главная страница Случайная лекция


Мы поможем в написании ваших работ!

Порталы:

БиологияВойнаГеографияИнформатикаИскусствоИсторияКультураЛингвистикаМатематикаМедицинаОхрана трудаПолитикаПравоПсихологияРелигияТехникаФизикаФилософияЭкономика



Мы поможем в написании ваших работ!




Корректность и полнота метода резолюций

Читайте также:
  1. II. Проблема источника и метода познания.
  2. БУХГАЛТЕРСКИЕ СЧЕТА КАК ЭЛЕМЕНТ МЕТОДА БУХГАЛТЕРСКОГО УЧЕТА
  3. В настоящий момент метод Короткова принят во всем мире в качестве стандартного метода измерения артериального давления.
  4. Вопрос 1. Общие сведения о методах измерения частоты
  5. Выбор метода организации ТО и ТР автомобилей
  6. Выбор метода получения заготовки
  7. Выбор метода получения заготовки
  8. Выбор метода управления в зависимости от инерционности нагрузки
  9. Выбор метода численного решения многокритериальных задач.
  10. ДОКУМЕНТИРОВАНИЕ ХОЗЯЙСТВЕННЫХ ОПЕРАЦИЙ КАК ЭЛЕМЕНТ МЕТОДА БУХГАЛТЕРСКОГО УЧЕТА

Корректность метода резолюций доказывается тем, что множество дизъюнктов S невыполнимо тогда и только тогда, когда существует резолютивный вывод пустого дизъюнкта из S, так как пустой дизъюнкт не может быть истинным ни при какой интерпретации.

Пусть из S существует резолютивный вывод пустого дизъюнкта. Докажем, что S невыполнимо. Поскольку резольвента R есть логическое следствие порождающих ее дизъюнктов Di и Dk, то конъюнктивное присоединение резольвенты R к конъюнкции дизъюнктов Di и Dk не меняет ее логическое значение. Если в множестве резольвент S имеется пустая резольвента (дизъюнкт ранга 0), то множество S невыполнимо, поскольку соответствующая множеству R(S) КНФ содержит ложный логический сомножитель (дизъюнкция ранга 0 ложна по определению).

Полнота метода резолюций состоит в том, что он гарантирует получение пустой резольвенты, если множество дизъюнктов S невыполнимо. Если же пустая резольвента не найдена, то множество S не является невыполнимым.

Теорема. Множество дизъюнктов S противоречиво тогда и только тогда, когда существует опровержение S.

Корректность метода резолюций очевидна, так как пустой дизъюнкт не может быть истинным ни при какой оценке.

Правило резолюций имеет свойство полноты в том смысле, что позволяет вывести из множества дизъюнктов пустой дизъюнкт, если исходное множество дизъюнктов S противоречивое.

Отношение выводимости компактное вследствие конечности вывода.

 

Литература

  • Чень Ч., Ли Р. Глава 5. Метод резолюций // Математическая логика и автоматическое доказательство теорем = Chin-Liang Chang; Richard Char-Tung Lee (1973). Symbolic Logic and Mechanical Theorem Proving. Academic Press. — М.: «Наука», 1983. — С. 358.
  • Нильсон Н. Дж. Принципы искусственного интеллекта. — М., 1985.
  • Мендельсон Э. Введение в математическую логику. — М., 1984.

· Рассел С., Норвиг П. Искусственный интеллект: современный подход = Artificial Intelligence: a Modern Approach. — М.: Вильямс, 2006.

 


[1] О.Е. Акимов. Дискретная математика. Логика, группы, графы. М.: Лаборатория базовых знаний, 2003. – 376 с. (с. 41).


<== предыдущая страница | следующая страница ==>
Корректность и полнота логического вывода | Введение. Анализ влияния форм и методов розничной торговли на принятие потребителем решения о покупке продовольственных товаров

Дата добавления: 2014-11-08; просмотров: 375; Нарушение авторских прав




Мы поможем в написании ваших работ!
lektsiopedia.org - Лекциопедия - 2013 год. | Страница сгенерирована за: 0.002 сек.