26Теорема дедукции. Связь выводимости и истинности формул в логике высказываний. Выполнимые и общезначимые формулы.

Если из системы гипотез Г и А выводится В, то из системы гипотез Г выводится А->В и наоборот.

Высказыванием является повествовательное предложение, которое формализует некоторое выражение мысли. Это утверждение, которому всегда можно поставить в соответствие одно из двух логических значений: ложь или истина. Логическая формула – это составное высказывание, состоящее из элементарных высказываний, соединенных связками. Формула A называется общезначимой, если во всех своих интерпретациях она принимает значение «истина». Выполнимыми называются формулы, допускающие указание интерпретации, в которой эта формула истинна.

27Понятие логического следования, принцип дедукции. Правило резолюций, метод резолюций. Стратегии метода резолюций.

Логическое следование – это отношение, существующее между посылками и обоснованно выводимыми из них заключениями. Отношение - математическая структура, которая определяет свойства объектов и их взаимосвязи. Принцип дедукции. Формула B является логическим следствием конечного множества A тогда и только тогда, когда A È {ØB } невыполнимо.

{A₁, …, A_n}|— B Û { A₁, …, A_n, ØB}|— 0.

Для порождения логических следствий используется очень простая схема рассуждений. Пусть А, В, X — формулы. Предположим, что две формулы (A Ú X) и (B Ú ØX) – истинны. Если X — истинна, то следовательно В истинна. Наоборот, если X ложна, то можно заключить, что А — истинна. В обоих случаях (A Ú В) истинна. Получается правило

{AÚX, BÚØX} |— A Ú В,которое можно записать в виде{ØX Ú A, X Ú B} |— A Ú В.Это правило называется правилом резолюций. Для любых дизъюнктов С и С*, если существует литера L в С, контрарная литере L* в С*, то вычеркнув L и L* из С и С* соответственно, построим дизъюнкцию оставшихся членов. Построенный дизъюнкт называется резольвентой С и С*.

28Методы анализа выполнимости и общезначимости формул: семантическое дерево, тривиальный алгоритм, алгоритм Квайна, алгоритм редукции, алгебраический подход, метод Девиса-Патнема, метод резолюций, фразы Хорна.

Тривиальный метод (найти значения при всех возможных интерпретациях).

Алгебраический метод (применение законов булевой алгебры логики).

Метод редукции (проверка формул путем сведения к абсурду).

Метод Куайна (обобщение тривиального алгоритма).

Метод резолюций:строим формулу F=p*|R. Приводим F к КНФ. КНФ ставим множество дизъюнктов. Применяя правило резолюций, получаем резольвенту, добавляем в множество дизъюнктов. Если резольвента пуста, тогда множество диз противоречиво.

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

(А₁ Ú L) & …& (A_m Ú L) & (B₁ Ú ØL) & … &(B_n Ú ØL) &R, где A_i, B_i и R чисты от L и ØL, S₁ = А₁ & …& A_m &R и S₂= B₁ & … &B_n &R, то S противоречиво тогда и только тогда, когда (S₁ Ú S₂) противоречиво, т.е. S₁ и S₂ противоречивы.

Представим функцию импликации в виде минимальной ДНФ с помощью формулы;

A ® C º `A Ú C

(A₁&A₂& ¼&A_m) ® B Ú C будет соответствовать формула (с учётом правила де Моргана) `A<sub>1</sub> Ú`A₂ Ú ¼Ú`A<sub>m</sub> Ú B Ú C. Перенесём положительные литеры вперед и получим B Ú C Ú A<sub>1</sub> Ú`A₂ Ú ¼Ú`A<sub>m</sub>. Такую формулу называют фразой Хорна, положительные литеры (B,C) называют альтернативными следствиями, негативные (`A₁,`A<sub>2</sub>, ¼,`A_m )– необходимыми посылками.