34. Выводимость на основе противоречия. Приведение к кнф.

Теорема

Из F1,..,Fn|-G тогда и только тогда когда формула F1&F2&..Fn&~G является противоречием или равно всегда Л.

Доказательство.

По предыдущей теореме было показано, что F1..Fn |-G тогда и только тогда когда F1&F2&..Fn->G* является тавтологией. * является тавтологией тогда и только тогда когда отрицание не выполнимо ~(F1&F2&..Fn->G)=G. Импликацию раскрываем через дизъюнкцию, тогда получаем условие: ~(~(F1&F2&..Fn)vG)=Л. Отсюда следует по закону Де Моргана: F1&F2&..&Fn&~G=Л.

Конъюнктивной нормальной формой называется логическое произведение или конъюнкция дизъюнктов. Принято считать, что в дизъюнкте переменные и литералы не повторяются, т.к. LvL=L Lv~L=И. Считаем что в самой КНФ нет одинаковых дизъюнктов, т.к. C&C=C. В свою очередь КНФ можно записать, как множество дизъюнктов, т.е. пусть имеем F=C1&C2&..&Ck => F={C1,C2,..,Ck}. В результате вопрос о выводимости формулы G из F1,F2..Fn |-G сводится к вопросу о том, является ли тождественной ложью представление формулы F1&F2&..&Fn&~G в виде КНФ. Для приведения формулы к виду КНФ используется известные тождества булевой алгебры.

A&(BvC)=A&BvA&C

Av(B&C)=(AvB)&(AvC)

Av~A=И

A&~A=Л

AVИ=И

A&И=A

AvЛ=А

А&Л=Л

A->B=~AvB

~(AvB)=~A&~B

~(A&B)=~Av~B

A==B=(A->B)&(B->A)

Av(A&B)=A

A&(AvB)=A

35. Понятие резольвенты.

Резольвентой двух дизъюнктов С1 и С2, в которых 1 и только 1 литерал входит в один из дизъюнктов напрямую С1=L1vL2v..vLk, С2=~L1vL2`v..vLm`

Обозначаем R(C1,C2) – дизъюнкт, составленный из литералов дизъюнктов С1 и С2 за исключением литерала, входящего с противоположным знаком. Литерал L1 и L2 называют контрарной парой. R(C1,C2)=L2v..vLkv L2v`..vLkv`

Если рассматривать с точки зрения множеств, то запишем R(C1,C2)=(C1/{L,~L})v(C2/{L,~L}). В вырожденном случае, когда каждый из дизъюнктов представлен одним литералом, т.е. в КНФ есть запись вида: &{L}&..&{~L} резольвента этих дизъюнктов R(C1,C2)=0 пустой дизъюнкт. Присутствие таких дизъюнктов, как L и ~L говорит о ее противоречивости. Таким образом, то, что резольвента некоторых 2-х дизъюнктов дает пустое множество, является признаком противоречивости КНФ. Замечание: при поиске дизъюнктов, для которых находятся резольвенты, важным является условие наличия в них ровно 1 контрарной пары. Пусть, например, С1=~AvB C2=Av~B, то C1&C2=И. Нам нужно доказать противоречивость формулы. Поэтому попытка найти резольвенту от дизъюнктов, в которых более одной контрарной пары не имеет смысла в рамках метода резолюций.

Лемма. Резольвента является логическим следствием своих дизъюнктов.

R=R(C1,C2) тогда C1&C2->R=И

Доказательство:

Если R является резольвентой C1 и C2, то исходные дизъюнкты представимы в виде: C1=L1vL2v..vLk C2=L1`vL2`v..vLk`. Если С1&C2=Л, то формула условия теоремы истинна. Пусть 1) C1&C2=Л => C1&C2->R=И L1`=~L1

2) Если истинным является один из литералов L2..Lk, то этот литерал войдет в резольвент => импликация истинна. Если C1 истинно за счет литерала L1, то т.к. C2 тоже истинно, она истинна за счет какого-то другого литерала кроме контрарного. С2 истинно за счет литерала L2`..Ln`, а он тоже войдет в резольвенту. Так, когда С1& C2 истинна, то резольвента тоже истина, значит формула C1&C2->R тавтология.

Следствие: Пусть дана С1&C2&..&Cn, R=R(Ci,Cj). Тогда исходная КНФ == КНФ вида C1&C2&..&Cn&R. Поскольку, когда исходная КНФ ложна, то и новая КНФ ложна. Когда исходная КНФ истинна, то истинны два любых дизъюнкта, значит истинна их резольвента. Пусть C1,C2,..,Cn – набор дизъюнктов, тогда резолютативным выводом называется цепочка A1,A2,..,Ak, где Ai или исходных дизъюнкт или получен из предыдущих в виде резольвенты. Т.к. резольвента может быть добавлена к КНФ, для проверки на противоречивость, можем порождать резольвенты, пока не получим пустой дизъюнкт или не придем к невозможности породить новые резольвенты. В образовании резольвент участвуют резольвенты, полученные на предыдущих шагах.