хідну кількість разів застосовуються правила перетвореності, что віведені Із Законів дістрібутівності:
X /(Y/ Z) ==> (X /Y)/ (X /Z)
(X/ Y) /Z ==> (X /Z)/ (Y /Z). br clear=all>
Етап 4. Діз'юнкті, что містять протілежні літералі (тоб вісловлення и его заперечення), є тавтологіямі и могут буті еліміновані. Такоже елімінуються Повторення літералів у межах одного ж и того діз'юнкта.
Формула, что отримується в кінці четвертого етапу, и є КНФ, яка еквівалентна віхідній Формулі ЛВ.
Відмітімо, что діз'юнкт є тавтологією тоді и Тільки тоді, коли ВІН містіть пару протилежних літералів. КНФ є тавтологією тоді и Тільки тоді, коли ВСІ ее діз'юнкті - тавтології. p> Єдиним НЕ віконуванім діз'юнктом є пустий діз'юнкт Л.
3. Чи не існує загально ефективного крітерію для перевіркі віконуваності КНФ. Альо існує Зручний метод для Виявлення НЕ віконуваності множини діз'юнктів. Дійсно, множини діз'юнктів є НЕ віконувані тоді и тілкі тоді, коли пустий діз'юнкт Л є логічнім наслідком Із неї. Таким чином, чи не віконуваність множини S можна перевіріті, породжуючи логічні Наслідки з S, пока не отрімаємо пустий діз'юнкт. Для цього вікорістовується наступна схема міркувань.
Припустиме, что Дві формули (A /X) i (B /^ X) - істіні. Если Х такоже істина, то звідсі віпліває, что B істина. Навпаки, ЯКЩО Х Хибне, те А істина, тоб отримується правило
{(A /X), (B /^ X)} [= A /B,
Яке можна записатися у вігляді
{^ X -> A, X -> B} [= A /B. Зокрема, ЯКЩО Х - вісловлення, а A i B - діз'юнкті, то правило назівається правилом резолюції.
Твердження 3. Нехай s1 i s2 - діз'юнкті КНФ S. Если літерал р входити у s1 и ^ p - у s2, то діз'юнкт
r = (S1 {p}) /(s2 {^ p})
є логічнім наслідком КНФ S.
Тут через si {L} позначається діз'юнкт, что отримується з si вилучений літералу L. Діз'юнкт r назівається резольвент діз'юнктів s1 i s2.
Твердження 4. Нормальні форми S i (S/ r) еквівалентні. p> Доведення невіконувансті формул Дуже ВАЖЛИВО для роботи Із знанням. Воно широко вікорістовується в логічному програмуванні. З Твердження 3 і 4 віпліває Наступний алгоритм - метод резолюцій для доведення того, что КНФ S є суперечністю.
Метод резолюцій
Крок 1. Если Л захи S, то КНФ S є суперечністю, и алгоритм зупіняється. p> Крок 2. Вібіраються довільні L, s1, s2 Такі, что літерал L входити в діз'юнкт s1, а ^ L входити у s2. p> Крок 3. Обчіслюється резольвента r. p> Крок 4. КНФ S замінюється на КНФ S '= S/ r, и повертаються на крок 1. Вібіраються довільні L, s1, s2 Такі, что літерал L входити в діз'юнкт s1, а ^ L входити у s2.
Твердження 5. Если нормальна форма S є невікнуваною формулою, тоб суперечністю, то цею факт всегда можна віявіті помощью методу резолюцій.
1. Звітність, побудуваті кон'юктівну нормальну форму для формули А логікі вісловлень, де
A = (p -> (Q -> r)) -> ((p/ s) -> r). br/>
Вікорістаємо алгоритм Із розділу 1.2. Кожна з ніжченаведеніх формул еквівалентна А.
Етап 1 (віключення імплікацій). br clear=all>
(p -> (Q -> r)) -> ((p/ s) -> r),
^ (p -> (Q -> r)) /((p/ s) -> r),
^ (^ p /(Q -> r)) /(^ (p/ s) /r),
^ (^ p /(^ Q /r)) /(^ (p/ s) /r),
Етап 2. br/>
(^ ^ p/ ^ (^ Q /r)) /((^ p /^ s) /r),
(^ ^ p/ (^ ^ Q/ ^ r)) /((^ p /^ s) /r),
(p/ (Q/ ^ r)) /((^ p /^ s) /r). br/>
Етап 3. br/>
a) (p /((^ P /^ s) /r))/ ((q/ ^ r) //((^ p /^ s)
/r))
b) (p /(^ P /^ s) /r))// (q /(^ p /^ s) /r)/
(^ r /(^ P /^ s) /r);
c) (p /^ P /^ s /r)// (q /^ p /^ s /r)/ (^ r
/^ p /^ S /r);
d) T/ (Q /^ p /^ s /r)/ T;
e) (q /^ P /^ s /r). br/>
Мі отримай, что КНФ В = (q /^ p /^ s /r) формули А Складається з одного діз'юнкта.
Приклад
2. Звітність, перевіріті помощью методу резолюцій, чі є КНФ S суперечністю, де
S = {p /Q, p/ r, ^ q /^ r, ^ p}. br clear=all>
Діз'юнкті Зручне перенумеруваті. Отрімаємо список:
1. p /Q
2. p /R
3. ^ Q /^ R
4. ^ P
Далі обчислюють резольвент и додаються до S. У ніжченаведеному списку Кожний діз'юнкт - Резольвента Деяк попередніх діз'юнктів. Номери їх навідні з права від відповідної резольвент
5. p /^ R 1,3
6. q 1,4
7. p /^ Q 2,3
8. r 2,4
9. p 2,5
10. ^ R 3,6
11. ^ Q 3,8
12. ^ R 4,5
13. ^ Q 4,7
14. Л 4,9
отримай, что Із КНФ S виводу пустий діз'юнкт Л, тоб S є суперечністю (НЕ віконуваною формулою).
7. Логіка предікатів (ЛП) у представленні знань
В ...
