= І за рахунок якогось литерала крім L = > цей літерал увійде і в R => R = І => імплікація - І.
Слідство: Нехай дана КНФ З 1 & ... & C n і резольвента R = R (C i , C j ). Тоді ця формула КНФ C 1 & ... & C n Вє C 1 & ... & C n & R.
Доказ:
Якщо Л.Ч. = Л => п.ч. = Л
Якщо Л.Ч. = І => п.ч. = І (по лемі)
Зауваження: для перевірки на суперечливість КНФ (мн-ва диз'юнктів) можна породжувати резольвенти до тих пір, поки не отримаємо ТЛ.
резольвент знаходяться не тільки для вихідних диз'юнктів, а й для тих резольвент, кіт. породжуються.
Теорема про повноту методу резолюцій
Теорема про повноту методу резолюцій:
КНФ (безліч диз'юнктів) - протиріччя <=> з безлічі диз'юнктів виводиться резолютотівно порожній диз'юнкт.
Док-во:
Якщо виводимо порожній диз'юнкт, то формула - протиріччя. Це можливо тільки в тому випадку, якщо
C 1 = L, C 2 = Г№ L
Але тоді маємо КНФ: L Г№ L Вє Л.
{C 1 & ... & C n = C 1 & ... & C < span align = "justify"> n & R 1 = ... = C 1 & ... & C n & R 1 & ... & L & Г№ L Вє Л}
II
Нехай вихідна формула - протиріччя. Покажемо, що виводиться порожній диз'юнкт (по індукції). p align="justify"> Є C 1 , ..., C n
Виводиться пар-р K (S) = ГҐ (кол-во входжень всіх літералів) - n (кол -во диз'юнктів) аксіома резолюція протиріччя
Наприклад, КНФ: ( Г№ BVA) C (BV Г№ D) K (S) = 5 - 3 = 2
БІ: доведемо справедливість при K (S) = 0 (для всіх таких формул)
K (S) = 0 <=> формула має вигляд L 1 L < span align = "justify"> 2 ... L n Вє Л, тобто в диз'юнктів 1 літерал, КНФ - твір літералів <=> ця формула Вє < span align = "justify"> Л <=>, коли в ній є пара L і Г№ L => порожній диз'юнкт виводиться.
Індуктивний перехід: нехай ми довели для k ВЈ m. Доведемо для формули, у якої k = m + 1> 0.
Якщо K> 0 => 1 з диз'юнктів містить хоча б 2 литерала (нехай З 1 ).
З 1 = LVC 1 < span align = "justify">.
Вих. формула: S = C 1 & ... & C n < span align = "justify"> = C
