Главная | Обратная связь | Поможем написать вашу работу!

Корректность и полнота логического вывода

Доказательства корректности и полноты методов, применяемых в логике высказываний, содержатся в [1, 2, 3, 4, 5,].

Корректность и полнота метода семантических таблиц

Теорема корректности. Если высказывание s доказуемо по Бету, то оно логически истинно. Формальная запись:

├_В s Þ ╞ s.

Согласно определению, высказывание s доказуемо по Бету, если семантическая таблица с помеченной формулой fs в корне является противоречивой, т.е. противоречивы все ее ветви. Если высказывание s не является логически истинным, то найдется интерпретация (множество логических значений атомов), для которой в семантической таблице обнаружится непротиворечивая ветвь c. Однако в этом случае s не доказуемо по Бету.

Теорема полноты. Если высказывание s логически истинно, то оно доказуемо по Бету. Формальная запись:

╞s Þ├ _В s.

Значок ╞ означает общезначимость, т.е. ╞s означает, формула s истинна во всех возможных интерпретациях. Если высказывание s логически истинно, то для любой интерпретации I верно: I(s)=t.

Пусть высказывание s общезначимо. Построим для него семантическую таблицу с корнем f(s). Если высказывание s не выводимо по Бету, то в таблице окажется хотя бы одна противоречивая ветвь. Это означает, что в некоторой интерпретации высказывание s ложно, что противоречит общезначимости s.

Следовательно, доказательство по Бету для s обязано существовать.

Построение семантической таблицы для формулы s гарантирует, получение для формулы s либо доказательства, либо опровержения.

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

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

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

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

Корректность и полнота аксиоматической системы вывода

Сформулируем теоремы корректности, полноты и компактности аксиоматических методов.

Теорема корректности и полноты. Высказывание s выводимо из множества высказываний S тогда и только тогда, когда s-- логическое следствие S. Формальная запись:

S├s Û S╞ s.

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

⇐ Предыдущая 1 2 3 4 567 8 9 10 Следующая ⇒

Воспользуйтесь поиском по сайту: