• Аксіоматичні системи логік
  • 4.1. Система аксіом і правил виведення
  • 4.2. Випереджені нормальні форми
  • 4.3. Побудова доведень в аксіоматичній системі
  • 4.4. Метод ідентифікації
  • 4.5. Метод резолюцій

Аксіоматичні системи логік

Аналогічно числення висловлювань в аксіоматичній системі логік існує формальна система – числення предикатів, яка займається конструюванням формул і доведенням їх загальнозначущості. Числення предикатів, тобто формальна теорія предикатів будується за вищенаведеною класичною схемою побудови формальних теорій.

Аксіоматична система логік має ідентичну численню висловлювань структуру: мову, систему аксіом і правила виведення. Мова аксіоматичної системи логік складається з правильно побудованих формул логіки предикатів першого порядку, а опис аксіом і правил виведення наведений у наступному параграфі.

4.1. Система аксіом і правил виведення

Числення предикатів першого порядку визначають аксіоматичним шляхом. Аксіоми поділяють на два класи: логічні аксіоми і власні аксіоми, або нелогічні аксіоми. До логічних аксіом відносять аксіоми, які визначаються для будь-яких А, В, С схемами:

АП1) А→ (В → А);

АП2) (А → (В → С)) → ((А → В) → (А → С));

АП3) ( ¬ В → А) → (( ¬ В → А) → В);

АП4) х1А(х1) → А(t), де t – терм, вільний для змінної х1 у формулі А(х1);

АП5) х1 (А → В) → (А → х1В), якщо формула А не містить вільних входжень змінної х1.

Власні аксіоми, будучи визначеними, фіксують деяку конкретну теорію першого порядку, тому для спільного описання всіх теорій першого порядку вони не можуть бути сформульовані. Якщо власних аксіом немає, то таку теорію називають численням предикатів першого порядку і позначають ПL.

У численні предикатів першого порядку визначено два основні правила виведення:

П1) modus ponens (МР): із А і А→В випливає В;

П2) правило узагальнення: із А випливає хі А.

Поняття виведення із множини формул у теорії ПL визначають аналогічно численню висловлювань, але при цьому необхідно внести додаткове уточнення. Воно полягає в тому, що у виведенні формули В із множини формул Г змінна xi є фіксована, якщо в цьому виведенні ні разу не застосовувалося правило П2 узагальнення по змінній . У протилежному разі кажуть, що змінна у даному виведенні варіюється.

Для позначення факту наявності виведення формули В із множини формул Г, в якому всі змінні, xj,…xjz фіксовані, використовують запис Г ├ х_j,.....x_jz В. Інакше кажучи, у цьому записі указують, що правило узагальнення використовують тільки по змінних х_j,.....x_jz.

Приклад 4.1.1. Вивести формулу А( а₀, х₂) із формули А(х₁, х₂).

Розв’язання. Для виведення формули застосуємо правило узагальнення й із А(х₁, х₂) одержимо х₁ А(х₁, х₂). Згідно з аксіомою АП4 запишемо аксіому

x₁ А(х₁, х₂)→А(х₀, х₂).                                                                   (4.1.1)

Одержана формула х₁ А(х₁, х₂) разом з 4.1.1 по МР дозволяє вивести

А( а₀,х). У побудованому виведенні змінна х1 варіюється. Тоді виведення формули можна записати у такому вигляді А(х₁, х₂) ├x₁ А₁ (,).

Як зазначалося вище, в логіці предикатів першого порядку визначені два основні правила виведення: П1), П2), але з розділів 1 і 2 можна зробити висновок, що для можливості скорочення довжини виведення необхідно розширити множину правил виведення. Розглянемо деякі з них, які можуть бути застосовані при виведенні формул у логіці предикатів першого порядку.

Їх можна розділити на дві групи. До першої відносять такі структурні правила виведення.

1. Закон тотожності

А ├ А

2. Правило введення, яке формулюється так: якщо Г ├ А, то Г, В ├ А. Для наглядності його, а в подальшому й усі інші, будемо записувати у вигляді

Г ├ А____

Г, В├ А

3. Правило перестановки

Г, В, С, ∆├ А

Г, С, В ,∆ ├ А

4. Правило скорочення

Г, В, В, ∆├ А

Г, В, ∆├ А

5. Правило перетину

Г├ ∆, А├ В

Г, ∆├ С

До другої групи відносять логічні правила виведення, які, у свою чергу, можна розбити на групи, для яких є логічні зв’язки і квантори зі своєю групою правил. Крім того, усередині кожної групи правила ділять на два види: правила введення, які показують доведення формули з даним логічним символом, і правила вилучення, які показують використання формули з даним логічним символом для доведення інших формул.

1. Правило диз’юнкції:

введення                                                                     вилучення

Г├ А _____.                  Г├ В ___.                               Г, А ├ С; Г, В ├ С

Г├ АВ ’                    Г├ АВ ’                                 Г, А В ├ С ˙

 

2. Правило кон’юкції:

введення                                                                        вилучення

Г ├ А; Г ├ В .                                                                   Г, А, В ├ С

Г ├ А В ’                                                                      Г, А В ├ С ˙

3. Правило імплікації:

введення                                                                        вилучення

 Г, А ├ В ___.                                                               Г├ А; Г ├ А → В

Г ├ А → В ’                                                                         Г ├ В ˙

4. Правило еквівалентності:

введення                                                                        вилучення

 

Г, А ├ В; Г, В ├ А .                                                           Г ├; Г ├ А ~ В .

Г ├ А ~ В ’                                                                            Г ├ В ’

 

                                                                                       Г ├ В; Г ├ А ~ В

                                                                                             Г ├ А ˙

5. Правило заперечення:

введення                                                                        вилучення

Г, А ├ В; Г, А ├ ¬ В .                                                       Г ├ ¬¬ А

Г ├ ¬ А ’                                                                            Г ├ А ˙

6. Правило узагальнення:

введення                                                                         вилучення

Г ├ А (у)____  .                                                               Г ├ [TEX]\forall [/TEX]х А (х)

Г ├ х А (х) ’                                                                 Г ├ А (у) ˙

У формулі введення квантора загальності А (у) означає для довільного

у F, а саме правило стверджує істинність х А (х), якщо доведена істинність А (у) для будь-якого у, тобто для всіх елементів у з розглянутої предметності області F.

У формулі видалення квантора загальності А (у) означає для довільного у F, а саме правило використовується для доведення істинності А (у), де у – довільно обраний елемент предметної області F, у якій справедливе х А (х).

7. Правило існування:

введення                                                                          вилучення

Г├ А (у) __.                                                                      Г, [TEX]\exists [/TEX]х А (х) ├ С

х А (х) ’                                                                          Г, А (у) ├ С ˙

У формулі вилучення квантора існування А (у) означає для деякого у F, а саме правило дозволяє вирішити, що х А (х) є істинним тоді і тільки тоді, коли відомий деякий елемент у, для якого істинне А (у).

У формулі вилучення квантора існування А (у) означає для деякого у F, а саме правило полягає в позначенні імені елемента у, для якого А (у) є істинне.

Усі розглянуті вище правила відповідають звичайним прийомам математичного міркування. Наприклад, у правилі існування вилучення квантора відповідає правилу одиничного вибору. Припустимо, що є х А (х) і необхідно вивести С. Оскільки є х таке, що А (х), то можна розглянути (вибрати) одне із таких х. Позначимо його через у. А це означає, що для цього у дійсне

А (у). Таким чином, достатньо вивести формулу С із А (у). Аналогічно можна розглянути й інші правила.

8. Правило перейменування вільних змінних

У логіці предикатів у виведенні формули А (х), що містить вільні входження х, жодне з яких не знаходиться в області дії квантора за у, виходить вивідність А (х).

Приклад 4.1.1. Довести справедливість правила перейменування вільних змінних.

Розв’язання.

а) А (х) – гіпотеза;

б) А (х) → ( В → А (х)) – аксіома АП1: тут як В можна обрати будь-яку довідну формулу, яка не містить вільних входжень змінних х;

в) В → А (х) – МР, із а), б) ;

г) В → x А (х) – правило узагальнення із в) ;

д) x А (х) – наслідок з кроку г), оскільки В – істинна формула ;

у) А (у) – аксіома АП4 із д) .

9. Правило перейменування пов’язаних змінних

У логіці предикатів у виведенні x А (х) виходить вивідністьy А (у), а у виведенні x А (х) – вивідність y А (у) за умови, що А (х) не містить вільних входжень у, а містить вільні входження х, жодне з яких не входить до області дії квантора за у.

Приклад 4.1.2 Довести правило перейменування пов’язаних змінних для квантора загальності.

Розв’язання.

а) x А (х) – гіпотеза ;

б) x А (х) → А (у) – аксіома АП4 ;

в) x А (х) → y А (у) – правило узагальнення із б) ;

г) x А (у) – МР із а), в) .

Приклад 4.1.3 Довести правило перейменування пов’язаних змінних для квантора існування.

Розв’язання

а) А (у) – гіпотеза;

б) А (у) → х А (х) – правило 7;

в) у А (у) → х А (х) – правило існування із а) і б);

г) х А (х) – МР із а) і в).

4.2. Випереджені нормальні форми

У логіці висловлювань було введено дві нормальні форми: кон’юнктивна і диз’юнктивна. В аксіоматичній системі логік вводиться третя нормальна форма, яку називають випередженою нормальною формою.

Означення 4.2.1. Формула Ф у логіці предикатів знаходиться у випередженій нормальній формі (ВНФ) тоді і тільки тоді, коли вона може бути зображена у вигляді ()… () (А), де () є або (х), або (х) і всі різні для різних і = 1, …, п, а А – формула, яка не містить квантора. Приставку () називають префіксом, а А – матрицею формули Ф. Якщо формула А залежить від вільної змінної х, то це записується як А (х), якщо ні, то – А.

Теорема 4.2.1. Для будь-яких формул F, G, H теорії числення першого порядку справедливі такі еквівалентності:

а) ¬х F(x) х (¬F (x));

б) ¬ х F(x) х (¬F(x));

в) х F(x) G х (F(x) G);

х F(x) G х (F(x) G);

г) х F(x) G х (F(x) G);

х F(x) G х (F(x) G);

д) х F(x) х Н (х) х (F(x) Н (х));

є) х F(x) х Н (х) х (F(x) Н (х));

ж) х F(x) х Н (х) х у (F(x) Н (у));

з) х F(x) х Н (х) х у (F(x) Н (у)).

Доведення . Виконаємо доведення еквівалентності а) ¬х F(x) х (¬F(x)). Нехай r – довільна інтерпретація на деякій області R. Якщо ¬ (х F(x)) істинна в інтерпретації r, то х F(x) хибна в r. Це означає, що існує такий елемент k(x) R, для якого F ( k (x) ) хибна, або те саме, що ¬F (k (x) ) істинна в r. Отже, х (¬F(x)) істинна в r.

Якщо ¬ (х F(x)) хибна в r, то х F(x) істинна в r. Це означає, що F(x) виконується на всіх послідовностях із R або що ¬F(x) не виконується на жодній такій послідовності з R. Отже, х (¬F(x)) хибна в r. Таким чином,

¬(х F(x)) х (¬F(x)).

Доведення еквівалентності б) аналогічне доведенню еквівалентності а).

Доведемо еквівалентність в) х F(x) G х (F(x) G). Нехай маємо х F(x) G ¬ (х F(x)) → G х (¬F(x)) → G.

Отже,

1) х (¬F(x)) → G – гіпотеза;

2) ¬F(x) → х (¬F(x)) – правило 7;

3) ¬F(x) → G – транзитивність із 1) і 2) ;

4) x (¬F(x) → G) x (F(x) G) – загальнозначність із 3).

І навпаки:

1) x (F(x) G) x (¬F(x) → G) – гіпотеза ;

2) ¬F(x) → G – правило 6 із 1;

3) (¬F(x) → G) → (¬G → F(x)) ‒ тавтологія ;

4) ¬G → F(x) – МР із 2) і 3) ;

5) x (¬G → F(x)) – узагальнення із 4 ;

6) х (¬G → F(x)) → (¬G → х F(x)) – схема аксіом АП5 ;

7) ¬G → x F(x) – МР із 5 і 6 ;

8) (¬G → x F(x)) → (¬x F(x) → G) – тавтологія ;

9) ¬x F(x) → G x F(x) G – МР із 7) і 8).

Доведемо спочатку першу еквівалентність г).

1) х F(x) G х (¬F(x)) → G – гіпотеза ;

2) (¬F(x)) → G – правило 6 ;

3) (¬F(x)) → G) → х (¬F(x) → G) – правило 7 ;

4) х (¬F(x) G) х (F(x) G) – МР із 2) і 3).

І навпаки:

1) х (¬F(x) → G) – гіпотеза;

2) х (¬F(x) → G) → (¬F(x) → G) – правило 7 ;

3) ¬F(x) → G – МР із 1) і 2) ;

4) x (¬F(x)) → ¬F(x) – правило 6 ;

5) x (¬F(x)) → G ¬x (¬F(x)) G х (F(x)) G – транзитивність із 3) і 4).

Доведення інших еквівалентностей із в) і г) тепер легко випливає із законів де Моргана.

x F(x) G ¬ (¬x F(x) ¬G) ((х¬F(x)) ¬G

¬(х (¬F(x) ¬G) ¬ (х ¬ (F(x) G) x (F(x)) G).

x F(x) G ¬ (¬x F(x) ¬G) (х (¬F(x)) ¬G)

¬(х (¬F(x) ¬G) ¬ (х ¬ (F(x) G) x (F(x) G).

Аналогічно доводяться й інші еквівалентності із г).

Доведення решти еквівалентностей пропонуються як вправи.

Теорема доведена.

Із теореми 4.2.1 випливає такий метод побудови ВНФ. Для зведення формули Ф до випередженої нормальної форми використовують такі дії:

а) вилучення логічних зв’язок “ →” і “” :

А В = (А → В) (В → А) ;

А → В = ¬ А В ;

б) вилучення і перенесення знака “ ¬” всередину формул:

¬(x F(x)) = х (¬F(x));

¬( х F(x)) = x (¬F(x));

¬¬F = F;

в) перенесення кванторів:

Q x Р(х) G = Q x (F(x) G);

Q x Р(х) G = Q x (F(x) G);

х F(x) х Н (х) = х (F(x) Н (х));

х F(x) х Н (х) = х (F(x) Н (х));

Q1 х F(x) х Н (х) = х у (F(x) Н (у));

Q1 х F(x) х Н (х) = х у (F(x) Н (у)).

Виходячи із методу побудови ВНФ, алгоритм отримання випередженої нормальної форми матиме такі кроки.

1. Вилучити логічні зв’язки еквіваленції “” та імплікації “ →” за допомогою правил а).

2. Перенести знак операції заперечення “ ¬” всередину формул, користуючись правилами: ¬ (F G) = ¬F ¬G; ¬ (F G) = ¬F ¬G,

і правилами б).

3. Виконати перейменування пов’язаних змінних, якщо є така необхідність.

4. Винести квантори на початок формули, використовуючи правила в).

Обґрунтуванням цього алгоритму є твердження, яке безпосередньо випливає з теореми 4.2.1.

Теорема 4.2.2. Алгоритм випередженої нормальної форми перетворює будь-яку формулу А теорії числення предикатів першого порядку АП в таку формулу В, яка знаходиться у ВНФ, що ├ А В у ПL.

Приклад 4.2.1. Звести формулу х F(x) → х Н (х) до ВНФ.

Розв’язання. Користуючись кроками 1, 2, 4 алгоритму, отримаємо

х F(x) → х Н (х) = ¬ (х F(x)) х Н (х) =х (¬F(x)) х Н (х) = х (¬F(x) Н (х)).

Приклад 4.2.2. Отримати ВНФ для формули

х у z (Р (х, у) Р(у, z)) → z R(x, y, z).

Розв’язання. Користуючись кроками 1, 2, 3, 4 алгоритму, отримаємо

х у z (Р (х, у) Р (у, z)) → z R(x, y, z) =

=(z y (¬z (Р(х, у) Р(у, z)) z R(х, у, z) =

=x y z (¬ Р(х, у) ¬ Р(у, z)) u R(х, у, и) =

= x y z u (¬ Р(х, у) ¬ Р(у, z) R(х, у, и)).

Оскільки матриця А формули Ф не містить кванторів, то її можна подати у кон’юнктивній нормальній формі (КНФ). Формула Р знаходиться у кон’юнктивній нормальній формі, якщо вона має вигляд Р = …,

де = … , і кожне ‒ це атомарна формула або її заперечення.

Алгоритм побудови КНФ має такі кроки.

1. 1. Вилучити зв’язки “” і “ →” з формули А за допомогою правила а), як в алгоритмі ВНФ.
2. 2. Вилучити подвійне заперечення за допомогою правила ¬ (¬F) = F, і перенести знак “ ¬” до атомів, користуючись законами де Моргана, як у алгоритмі побудови ВНФ.
3. 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.

4.3. Побудова доведень в аксіоматичній системі

Основною задачею аксіоматичної системи логіки предикатів є установлення істинності предикатних тотожностей і клауз. Позначимо через будь-який предикат із задовільним числом аргументів, а через ()‒ відповідну йому кванторну групу. Тоді, наприклад, закон дистрибутивності матиме такий вигляд

() (() () ) = (() () ) (() () ).

У тому, що він виконується для одномісних предикатів, можна переконатися за допомогою процедури конкретизації:

х = а, 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)]}.

Від того, що у квадратних дужках з’явиться замість диз’юнкції кон’юнкція і навпаки, а також замість одномісного предиката будуть фігурувати різні багатомісні предикати, – суть тотожності не зміниться. Вона залишиться істинною внаслідок справедливості законів логіки множин і принципу суперпозиції, який стверджує, що заміна будь-якої константи іншою константою або навіть групою констант не може вплинути на істинність тотожності.

Ті самі висновки можуть бути виконані й по відношенню до логіки висловлювань, яка відрізняється від логіки Буля аксіомою порядку

() , () ().

Процедура конкретизації зводить предикатну аксіому порядку до простого висловлювання, тому якщо клауза істинна для висловлювань, то вона буде істинною і для предикатів.

4.4. Метод ідентифікації

Цей метод базується на перетворенні предикатної клаузи на клаузу логічного висловлювання, шляхом ідентифікації ідентичних квантованих предикатів. Алгоритм методу ідентифікації має такі кроки.

1. 1. Виділити однойменні квантовані предикати, позначивши їх відповідними літерами формул логіки висловлювань.
2. 2. Перетворити предикатну клаузу на клаузу логіки висловлювань, записавши її за допомогою ідентифікованих літер формул логіки висловлювань і замінивши при цьому всі логічні зв’язки розглянутої предикатної клаузи.
3. 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 Р(и, и).

Використовуючи другий крок алгоритму, робимо перетворення предикатної клаузи у клаузу логіки висловлювань:

1. → , або ¬_, , ¬0.
2. Згідно з методом резолюції, § 2.7 суперечності можливі, якщо можливі дві інші суперечності, що випливають із клаузи логіки висловлювань:
3. , ¬ 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.

Подання їх предикатними суперечностями

1. [TEX]\forall [/TEX]z y А (z, z), ¬ х A(b, x) 0;
2. [TEX]\forall [/TEX]u v B (v, u), ¬ z B(z, z) 0;
3. [TEX]\forall [/TEX]z x B(x, z), ¬ x y B(x, y) 0

підтверджує істинність предикатної клаузи.

4.5. Метод резолюцій

В основу цього метода покладено не лише перетворення предикатної клаузи на клаузу логічного висловлювання, а подання останньої у вигляді кон’юктивної нормальної форми (КНФ) і суперечності. Алгоритм методу резолюцій має такі кроки.

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.

Звідси і випливає істинність предикатної клаузи.