Приклади аудиторних і домашніх завдань

Приклад 1:

Нехай S - ССФ формули F. Якщо F суперечлива, то по теоремі 3 F=S. Якщо F несуперечлива, то F не еквівалентна S. Довести це твердження.

Доведення. Нехай, наприклад, . Зрозуміло, що S - стандартна форма формули F. Виберемо інтерпретацію I у такий спосіб:

Область: D={1,2}.

Значення для а: а = 1.

Значення для P: Р(1) = 0, Р(2) = 1.

Тоді зрозуміло, що F істинна в I, оскільки P(x) ¹ Þ ($x)P(x)=1. Однак S ложна в I, оскільки a=1(P(a)=P(1)=0. Таким чином, F¹S.

4. Перевірити невыполнимость множини диз’ъюнктів {PÚQ, PÚR, ùQÚùR, ùP}.

Розв’язання. Використовуємо метод резолюцій. Випишемо вихідну множину диз’ъюнктів:

Алгоритм перевірки невыполнимости в загальному випадку не детермінований. Ми можемо вибирати S₁, S₂ і L різними способами. Наприклад, якщо вибирати диз’ъюнкти в лексикографічному порядку зростання їхніх номерів, одержимо следующюу послідовність виводу:

(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).

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

(5) Q (з 1 та 4),

(6) R (з 2 та 4),

(7) ùQ (з 3 та 6),

(8) Л (з 5 та 7).

Зрозуміло, що обрана стратегія може значно впливати на виконання алгоритму. Відзначимо дві важливі властивості алгоритму, що не залежать від обраної стратегії: 1) Якщо множина S не містить диз’юнктів, до яких можна застосувати схему резолюцій, то вона виконувана, за винятком тих випадків, коли ця множина містить порожній диз’юнкт. Інтерпретація I одержується заданием атома P=1 тоді і тільки тоді, коли P присутній у формулі без отрицания. Наприклад: (1) PÚùS, (2) PÚùD. При інтерпретації P=1, S=0, D=0 (PÚùS)Ù(PÚùD)=1; 2) Якщо алгоритм закінчив роботу після породження порожнього диз’юнкта, то встановлена невыполнимость вихідної множини диз’юнктів S.

5. Перевірити невыполнимость множини диз’юнктів

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

(5) Q (з 1 та 2),

(6) ùQ (з 3 та 4),

(7) Л (з 5 та 6).

Так як отримано Л, то S невыполнимо. Зазначений вивід представлений деревом на рис.12.1, що називається деревом виводу:

PÚQ ùPÚQ PÚùQ ùPÚùQ

Q ùQ

Л

Рисунок 12.1 – Дерево виводу

6. Дано наступну множину формул:

F₁: ("x)(C(x)®(W(x)ÙR(x))),

F₂: ($x)(C(x)ÙO(x)),

G: ($x)(O(x)ÙR(x)).

Довести, що G є логічним наслідком F₁ і F₂.

Розв’язання. Перетворимо F₁, F₂ і ùG у стандартну форму. У результаті отримаємо наступні п'ять диз’юнктів:

(5) ùO(x)ÚùR(x) з ùG.

Це множина диз’юнктів невыполнимо. Це можна довести за допомогою методу резолюцій, застосувавши підстановку q={a|x} до даної множини диз’юнктів. Таким чином отримаємо:

(1) ùC(a)ÚW(a),

(2) ùC(a)ÚR(a),

(3) C(a),

(4) O(a),

(5) ùO(a)ÚùR(a).

(6) R(a) резольвента (3) і (2),

(7) ùR(a) резольвента (5) і (4),

(8) Л резольвента (7) і (6).

Таким чином, G - логічний висновок F₁ та F₂.