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.

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

Контрольні запитання

1. У чому різниця пропозиційної логіки від аксіоматичної системи логік?

2. Які аксіоми має аксіоматична система логік?

3. Запишіть формули аксіом аксіоматичної системи логік.

4. Які правила виведення є спільними для пропозиційної логіки та аксіоматичної системи логік?

5. На які групи та підгрупи діляться правила виведення?

6. Для яких цілей використовують правила введення і правила вилучення?

7. Які обмеження необхідні для правил узагальнення та існування? Які можуть бути наслідки, якщо не дотримуватися зазначених обмежень?

8. Сформулюйте правило перейменування вільних змінних.

9. У чому сутність правил перейменування зв’язних змінних?

10. Дайте визначення випередженої нормальної форми.

11. Сформулюйте алгоритм перетворення виразів довільної форми у ВНФ.

12. Сформулюйте алгоритм подачі матриці А формули Ф у кон’юнктивній нормальній формі.

13. Що є основною задачею логіки предикатів?

14. Який закон використовують для побудови доведень у логіці предикатів?

15. Закони яких теорій використовують при побудові доведень у логіці предикатів і чому?

16. На якому принципі базується метод ідентифікації?

17. Сформулюйте алгоритм методу доведення предикатних клауз методом ідентифікації.

18. За яких умов і для яких предикатних клауз або тотожностей можна застосовувати алгоритм ідентифікації?

19. Які основні принципи покладені у метод резолюцій?

20. Сформулюйте алгоритм методу доведення предикатних клауз методом резолюцій.

21. За яких кінцевих умовах предикатна клауза буде істинною, а при яких – хибною?

Задачі для самостійного розв’язування

1. Довести, що

а) ├ x y А → y x А;

б) ├ x (А → В) → ( x А → x В).

2. Довести, якщо терм і вільний для змінної х у формулі А (х), то

а) x А (х) ├ А (t); б) А (t) ├ x А (х).

3. Довести, що для будь-яких формул А і В:

а) А, В ├ А В; б) А → С, В → D, А → В ├ С → → D; в) ├ А В ~ ( А В).

4. Звести до ВНФ такі вирази:

а) y x(А(х) → В(у)); б) x yВ(х, у) x А(х); в) x А(х) → ( x (В(у) y С(х, у)).

5. Задані формули:

а) ( Р Q) → R; б) (Р (R → Q)) → S;

в) ( Р Q) → ( R S);

перетворити у КНФ.

6. Істинність заданих предикатних клауз довести методом ідентифікації:

а) x y Р(х, у) → v u Р(и, v), x v P(x, v)  х y P(x, y);

б) x y Р(х, у) → u v Р(v, u), х v P(x, v) → → y u P(y, u), v x P(x, v) y х P(x, y);

в) х y Р(х, у) → x y Q(x, y), y R(x, y) → → x y Q(x, y), x y R(x, y) х y P(x, y).

7. Довести істинність предикатних клауз методом резолюцій:

а) [ x y P(x, y) → xQ(x)] → [ x yP(x, y)

 x y P(x, y)] y P(x, y) x y P(x, y);

б) x Р(х, у) → y Р(х, у) → x y Q(x, y), yP(x, y) → y P(x, y), yP(x, y) x P(x, y) → → y x Q(x, y);

в) x y Р(х, у), x y Р(х, у) → y Q(y),

x Q(x) [ y x P(x, y) → x y P(x, y)],

x Q(x) → x Q(x, y) y P(x, y).

Коментарі. У цьому розділі система аксіом і правил виведення взяті з [14, 19, 20]. Більш детальне викладення цього матеріалу можна знайти в [12, 27]. Властивості числення предикатів першого порядку і випереджені нормальні форми випливають з [27], а побудова доведень узята з [1, 7, 23, 26].

112