Перевірка правильності міркування шляхом побудови двійкової діаграми рішень

Розглянемо задачу (2) про логічне слідування (див. стор. 38). Формула BÚDÚH є логічним наслідком формул A®B, C®D, G®H, AÚCÚG, якщо формула F = (A®B)Ù(C®D)Ù(G®H)Ù(AÚCÚG)ÙØ(BÚDÚH) є суперечніс-тю. Формула F є суперечністю тоді й тільки тоді, коли упорядкована приведена ДДР, побудована за цією формулою, буде мати вигляд:

       Отже, побудуємо упорядковану приведену ДДР формули F й за її виглядом визначимо, чи є F суперечністю.

     Спочатку виберемо лінійний порядок на множині атомів, що входять у F. Нехай він буде таким: A<B<C<D<G<H. Розгалужуємо формулу F по A:

    F=AÞ F₁, F₀, де F₁=F[1/A], F₀=F[0/A], тобто

    F₁=(1®B)Ù(C®D)Ù(G®H)Ù(1ÚCÚG)ÙØ(BÚDÚH) = (1®B) Ù (C®D) Ù (G®H)Ù 1 Ù Ø(BÚDÚH) = (1®B) Ù (C®D) Ù (G®H)ÙØ(BÚDÚH);

    F₀=(0®B)Ù(C®D)Ù(G®H)Ù(0ÚCÚG)ÙØ(BÚDÚH) = 1Ù(C®D)Ù(G®H)Ù(CÚG)ÙØ(BÚDÚH)=(C®D)Ù(G®H)Ù(CÚG)ÙØ(BÚDÚH).

Далі розгалужуємо формулу F₁ по B:

    F₁=BÞ F₁₁, F₁₀, де F₁₁=F₁[1/B], F₁₀=F₁[0/B], тобто

F₁₁=(1®1) Ù (C®D) Ù (G®H)ÙØ(1ÚDÚH) = 1 Ù (C®D) Ù (G®H)ÙØ1 = (C®D) Ù (G®H)Ù0=0;

F₁₀=(1®0)Ù(C®D)Ù(G®H)ÙØ(0ÚDÚH) = 0Ù(C®D)Ù(G®H)ÙØ(0ÚDÚH) = 0.

Розгалужуємо формулу F₀ по B:

    F₀=BÞ F₀₁, F₀₀, де F₀₁=F₀[1/B], F₀₀=F₀[0/B], тобто

    F₀₁ = (C®D)Ù(G®H)Ù(CÚG)ÙØ(1ÚDÚH) = (C®D)Ù(G®H)Ù(CÚG)ÙØ1 = (C®D)Ù(G®H)Ù(CÚG)Ù0 = 0;

    F₀₀ = (C®D)Ù(G®H)Ù(CÚG)ÙØ(0ÚDÚH) = (C®D)Ù(G®H)Ù(CÚG)ÙØ(DÚH).

Розгалужуємо формулу F₀₀ по C:

    F₀₀=CÞ F₀₀₁, F₀₀₀, де F₀₀₁=F₀₀[1/C], F₀₀₀=F₀₀[0/C], тобто

    F₀₀₁ = (1®D)Ù(G®H)Ù(1ÚG)ÙØ(DÚH) = (1®D)Ù(G®H)Ù1ÙØ(DÚH) = (1®D)Ù(G®H)ÙØ(DÚH);

    F₀₀₀ = (0®D)Ù(G®H)Ù(0ÚG)ÙØ(DÚH) = 1 Ù (G®H) Ù G ÙØ(DÚH) = (G®H) Ù G ÙØ(DÚH).

Розгалужуємо формулу F₀₀₁ по D:

    F₀₀₁ = DÞ F₀₀₁₁, F₀₀₁₀, де F₀₀₁₁=F₀₀₁[1/D], F₀₀₁₀=F₀₀₁[0/D], тобто

    F₀₀₁₁ = (1®1)Ù(G®H)ÙØ(1ÚH) = 1Ù(G®H)ÙØ1 = (G®H)Ù0 = 0.

    F₀₀₁₀ = (1®0)Ù(G®H)ÙØ(0ÚH) = 0Ù(G®H)ÙØ(0ÚH) = 0.

Розгалужуємо формулу F₀₀₀ по D:

    F₀₀₀ = DÞ F₀₀₀₁, F₀₀₀₀, де F₀₀₀₁=F₀₀₀[1/D], F₀₀₀₀=F₀₀₀[0/D], тобто

    F₀₀₀₁ = (G®H) Ù G ÙØ(1ÚH) = (G®H) Ù G ÙØ1 = (G®H) Ù G Ù0 = 0.

    F₀₀₀₀ = (G®H) Ù G ÙØ(0ÚH) = (G®H) Ù G ÙØH.

Розгалужуємо формулу F₀₀₀₀ по G:

    F₀₀₀₀ = GÞ F₀₀₀₀₁, F₀₀₀₀₀, де F₀₀₀₀₁=F₀₀₀₀[1/G], F₀₀₀₀₀=F₀₀₀₀[0/G], тобто

    F₀₀₀₀₁ = (1®H) Ù 1 ÙØH = (1®H) Ù ØH.

    F₀₀₀₀₀ = (0®H) Ù 0 ÙØH = 0.

Розгалужуємо формулу F₀₀₀₀₁ по H:

    F₀₀₀₀₁ = HÞ F₀₀₀₀₁₁, F₀₀₀₀₁₀, де F₀₀₀₀₁₁=F₀₀₀₀₁[1/H], F₀₀₀₀₁₀=F₀₀₀₀₁[0/H], тобто

    F₀₀₀₀₁₁ = (1®1)ÙØ1 = 1®0 = 0, F₀₀₀₀₁₀ = (1®0)ÙØ 0 = 0Ù1 = 0.

Побудуємо ДДР (рис.4):

Рис. 4

Дана ДДР не є приведеною, оскільки містить вершини виду

 

Вилучимо їх (тобто вершини F₁, F₀₀₁, F₀₀₀₀₁). Маємо (рис.5):

Рис.5

Діаграма не приведена (надлишковою є вершина F₀₀₀₀). Послідовно вилучаючи зайві вершини (F₀₀₀₀, F₀₀₀, F₀₀, F₀, F), отримаємо:

Отже, формула F є суперечною, а це означає, що формула BÚDÚH є логічним наслідком формул A®B, C®D, G®H, AÚCÚG. Таким чином, задане міркування є логічно правильним.

 

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

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

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

3. Які нормальні форми формул логіки висловлень й яким чином можна використати, щоб перевірити правильність міркування?

⇐ Предыдущая3456789101112Следующая ⇒

Поделиться: