1. Вилучити зв’язки “ 
” і “ →” з формули А за допомогою правила а), як в алгоритмі ВНФ.
2. Вилучити подвійне заперечення за допомогою правила 
( F) = F, і перенести знак “ ” до атомів, користуючись законами де Моргана, як у алгоритмі побудови ВНФ.
3. Для отримання нормальної форми формули А використати дистрибутивні закони:
F 
(G 
Н) = (F G) (F Н);
F (G Н) = (F G) (F Н).
Приклад 4.2.3. Задану формулу (Р (Q → R)) → S перетворити у КНФ.
Розв’язання. Використовуючи кроки алгоритму 1, 2 і 3, отримаємо
(Р (Q→R))→S=(Р ( Q R))→S= (Р ( Q R)) S = =( Р ( Q R)) S=( Р Q) ( Р R) S= = ( Р Q S) ( Р R S).
Приклад 4.2.4. Задану формулу (Р Q) → R перетворити в КНФ.
Розв’язання. Використовуючи кроки наведеного вище алгоритму, отримаємо (Р Q)→R= (Р Q) R = =( Р ( Q)) R = ( Р Q) R.
Побудова доведень в аксіоматичній системі
Основною задачею аксіоматичної системи логіки предикатів є установлення істинності предикатних тотожностей і клауз. Позначимо через 
будь-який предикат із задовільним числом аргументів, а через (
) ‒ відповідну йому кванторну групу. Тоді, наприклад, закон дистрибутивності матиме такий вигляд:
(
) 
((
) 
(
) 
) =
= (() () ) (() () ).
У тому, що він виконується для одномісних предикатів, можна переконатися за допомогою процедури конкретизації:
х = а, b; = 
x; = А(х);
у = с, d; = 
y; = В(у);
z = e, f; = z; = C(z);
[ А(а) А(b) ] {[ В(с) В(d) ] [ C(e) C(f) ]} = = {[ A(a) A(b) ] [ B(c) B(d) ]} {[ A(a) A(b) ] [ C(e) Ù C(f) ]}.
Від того, що у квадратних дужках з’явиться замість диз’юнкції кон’юнкція і навпаки, а також замість одномісного предиката будуть фігурувати різні багатомісні предикати, – суть тотожності не зміниться. Вона залишиться істинною внаслідок справедливості законів логіки множин і принципу суперпозиції, який стверджує, що заміна будь-якої константи іншою константою або навіть групою констант не може вплинути на істинність тотожності.
Ті самі висновки можуть бути виконані й по відношенню до логіки висловлювань, що відрізняється від логіки Буля аксіомою порядку
() , () 
() .
Процедура конкретизації зводить предикатну аксіому порядку до простого висловлювання, тому якщо клауза істинна для висловлювань, то вона буде істинною і для предикатів.
Метод ідентифікації
Цей метод базується на перетворенні предикатної клаузи на клаузу логічного висловлювання шляхом ідентифікації ідентичних квантованих предикатів. Алгоритм методу ідентифікації має такі кроки.
1. Виділити однойменні квантовані предикати, по-значивши їх відповідними літерами формул логіки висловлювань.
2. Перетворити предикатну клаузу на клаузу логіки висловлювань, записавши її за допомогою ідентифікованих літер формул логіки висловлювань і замінивши при цьому всі логічні зв’язки розглянутої предикатної клаузи.
3. Розглянути одержану клаузу логіки висловлювань на її істинність чи хибність, використовуючи один із методів пропозиційної логіки: розділи 2.4, 2.5, 2.6, 2.7.
Приклад 4.4.1. Довести істинність предикатної клаузи х у Р(х, у) → → v Р(а, v), x Р(а, х) → x y Р(у, х) u v Р(и, v) → v u Р(и, v) методом ідентифікації.
Розв’язання. Використовуючи перший крок алгоритму, введемо позначення:
А = х у Р(х, у) = u v Р(и, v);
В = v Р(а, v) = x Р(а, х);
С = x y Р(у, х) = v u Р(и, v).
Згідно з другим кроком алгоритму робимо перетворення предикатної клаузи на клаузу логіки висловлювань:
А → В, В → С А → С.
Доведення істинності клаузи логіки висловлювань виконано аксіоматичним методом у прикладі 4.3.2. Звідси випливає, що і предикатна клауза є теж істинною.
Приклад 4.4.2. Довести істинність тотожності
x y Р(х,у) u v Р(v, и) v u Р(v, и) y x Р(х, у) = x y Р(у, х) u v Р(и, v) методом ідентифікації.
Розв’язання. Згідно з першим кроком алгоритму введемо такі позначення:
А = х у Р(х, у) = v u Р(v, и) = u v Р(и, v);
В = u v Р(v, и) = y x Р(х, у) = x y Р(у, х).
Використовуючи другий крок алгоритму, робимо перетворення предикатної тотожності на тотожність алгебри Буля:
( А В) (А В) = В А.
Виконуючи елементарні логічні перетворення, отримаємо
В А = В А,
що підтверджує істинність предикатної тотожності.
Приклад 4.4.3. Довести істинність клаузи
v u Р(и, v) → u v Р(и, v), x y Р(х, у) Þ u Р(и, и) методом ідентифікації.
Розв’язання. Користуючись першим кроком алгоритму, введемо такі позначення:
= x y Р(х, у); 
= v u Р(и, v);
= u v Р(и, v); 
= u Р(и, и).
Використовуючи другий крок алгоритму, робимо перетворення предикатної клаузи у клаузу логіки висловлювань:
→ , або , , 0.
Згідно з методом резолюції, суперечності можливі, якщо можливі дві інші суперечності, що випливають із клаузи логіки висловлювань:
, 0, , 0.
Подання їх предикатними суперечностями
x y Р(х, у), v u Р(v, и) 0,
u v Р(и, v), u Р(и, и) 0
підтверджує істинність предикатної клаузи.
Приклад 4.4.4. Довести істинність клаузи
z В(z, z) → x y В(х, у), z y A(z, y) → → u v B(v, u), x A(b, x) z x B(x, z) Ù z y A(z, x) методом ідентифікації.
Розв’язання. Згідно з першим кроком алгоритму введемо такі позначення:
= z y A(z, y); = x A(b, x);
= u v B (v, u) = z x B(x, z);
= z B (z, z); 
= x y B(x, y).
Використовуючи другий крок алгоритму, перетворюємо предикатну клаузу у клаузу логіки висловлювань:
→ , → , .
Замінивши імплікацію і привівши клаузу до суперечності, отримаємо
, , 0.
Згідно з методом резолюцій суперечності можливе тоді й тільки тоді, коли можливі інші суперечності клаузи, що випливають із клаузи логіки висловлювань:
, 0, , 0, , 0.
Подання їх предикатними суперечностями
z y А (z, z), х A(b, x) 0;
u v B (v, u), z B(z, z) 0;
z x B(x, z), x y B (x, y) 0
підтверджує істинність предикатної клаузи.
Метод резолюцій
В основу цього методу покладене не лише перетворення предикатної клаузи на клаузу логічного висловлювання, а подання останньої у вигляді кон’юнктивної нормальної форми (КНФ) і суперечності. Алгоритм методу резолюцій має такі кроки.
1. Виділити однойменні квантові предикати, позначивши їх відповідними літерами формул логіки висловлювань.
2. Перетворити предикатну клаузу на клаузу логіки висловлювань, записавши її за допомогою ідентифікованих літер формул логіки висловлювань.
3. Перетворити формулу логіки висловлювань на КНФ і звести її до суперечності.
4. Виконати склеювання диз’юнктивних посилок, видаливши у них тавтологічні висловлювання або їх компонування, що приводить до суперечностей.
5. Якщо на кроці 4 алгоритму буде одержана загальна суперечність, то предикатна клауза істинна, а якщо ні – то хибна.
Приклад 4.5.1. Довести істинність клаузи
х у Р(х, у) → v Р(а, v), x Р(а, х) → x y Р(у, х) Þ u vР(и, v) → v u Р(и, v) методом резолюцій.
Розв’язання. Використовуючи перший крок алгоритму, введемо позначення
А = x y Р(х, у) = u v Р(и, v);
В = v Р(а, v) = x Р(а, х);
С = x y Р(у, х) = v u Р(и, v).
Згідно з другим кроком алгоритму виконаємо пере-творення предикатної клаузи на клаузу логіки висловлювань: А → В, В → С А → С.
Користуючись третім кроком алгоритму, перетворимо отриману клаузу логіки висловлювань у КНФ і зведемо її до суперечності
А В, В С, ( А С) 0.
На четвертому кроці алгоритму виконаємо склеювання першої і другої посилок, у результаті одержимо посилку А С, яку склеюємо з третьою посилкою. Результатом цього склеювання є загальна суперечність, тому предикатна клауза – істинна.
Приклад 4.5.2. Довести істинність клаузи
u Р(и, и, а) y z Р(у, у, z)
Þ q Р(q, c, q) q u P(b, u, q) q u Р(b, u, q)
методом резолюцій.
Розв’язання. Використовуючи перший крок алгоритму, введемо позначення: А = u Р(и, и, а); В = y z Р(у, у, z); 
= q Р(q, c, q); 
= q u P(b, u, q).
Користуючись другим кроком алгоритму, виконаємо перетворення предикатної клаузи на клаузу логіки висловлювань: А В ; .
Спростовуючи цю клаузу і використовуючи третій крок алгоритму, отримаємо А В, , 0.
Згідно із четвертим кроком алгоритму суперечність у даному висловлюванні можливе, якщо можливі дві інші суперечності:
А, 0 В, 0.
Тобто: u Р(и, и, а), q Р(q, c, q) 0;
y z P(у, у, z), q u P(b, u, q) 0.
Звідси і випливає істинність предикатної клаузи.
Контрольні запитання
1. У чому різниця пропозиційної логіки від аксіоматичної системи логік?
2. Які аксіоми має аксіоматична система логік?
3. Запишіть формули аксіом аксіоматичної системи логік.
4. Які правила виведення є спільними для пропозиційної логіки та аксіоматичної системи логік?
5. На які групи та підгрупи діляться правила виведення?
6. Для яких цілей використовують правила введення і правила вилучення?
7. Які обмеження необхідні для правил узагальнення та існування? Які можуть бути наслідки, якщо не дотримуватися зазначених обмежень?
8. Сформулюйте правило перейменування вільних змінних.
9. У чому сутність правил перейменування зв’язних змінних?
10. Дайте визначення випередженої нормальної форми.
11. Сформулюйте алгоритм перетворення виразів довільної форми у ВНФ.
12. Сформулюйте алгоритм подачі матриці А формули Ф у кон’юнктивній нормальній формі.
13. Що є основною задачею логіки предикатів?
14. Який закон використовують для побудови доведень у логіці предикатів?
15. Закони яких теорій використовують при побудові доведень у логіці предикатів і чому?
16. На якому принципі базується метод ідентифікації?
17. Сформулюйте алгоритм методу доведення предикатних клауз методом ідентифікації.
18. За яких умов і для яких предикатних клауз або тотожностей можна застосовувати алгоритм ідентифікації?
19. Які основні принципи покладені у метод резолюцій?
20. Сформулюйте алгоритм методу доведення предикатних клауз методом резолюцій.
21. За яких кінцевих умовах предикатна клауза буде істинною, а при яких – хибною?
