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

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

Пусть из S существует резолютивный вывод пустого дизъюнкта. Докажем, что S невыполнимо. Поскольку резольвента R есть логическое следствие порождающих ее дизъюнктов D_i и D_k, то конъюнктивное присоединение резольвенты R к конъюнкции дизъюнктов D_i и D_k не меняет ее логическое значение. Если в множестве резольвент 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; Нарушение авторских прав

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