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

Перевіримо суперечність формули

F=(A«ØB)Ù(BÚØC)Ù(ØA®ØC)Ù(AÚC)

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

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

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

F₁=(1«ØB)Ù(BÚØC)Ù(Ø1®ØС)Ù(1ÚС),

F₀=(0«ØB)Ù(BÚØC)Ù(Ø0®ØС)Ù(0ÚС).

    Далі розгалужуємо формули F₁ та F₀ по В.

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

F₁₁=(1«Ø1)Ù(1ÚØC)Ù(Ø1®ØС)Ù(1ÚС)=0Ù(1ÚØC)Ù(Ø1®ØС)Ù(1ÚС)=0, F₁₀=(1«Ø0)Ù(0ÚØC)Ù(Ø1®ØС)Ù(1ÚС)=1Ù(0ÚØC)Ù(Ø1®ØС)Ù(1ÚС)= (0ÚØC)Ù(Ø1®ØС)Ù(1ÚС).

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

F₀₁=(0«Ø1)Ù(1ÚØC)Ù(Ø0®ØС)Ù(0ÚС)=1Ù(1ÚØC)Ù(Ø0®ØС)Ù(0ÚС)= (1ÚØC)Ù(Ø0®ØС)Ù(0ÚС),

F₀₀=(0«Ø0)Ù(0ÚØC)Ù(Ø0®ØС)Ù(0ÚС)=0Ù(0ÚØC)Ù(Ø0®ØС)Ù(0ÚС)=0.

    Розгалужуємо формули F₁₀ та F₀₁ по С.

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

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

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

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

    Усі розгалуження виконано; побудуємо упорядковану ДДР формули F (див. рис.6). Дана ДДР не є приведеною (бо містить надлишкову вершину F₀₁). Вилучимо її (див. рис. 7). Тепер діаграма містить надлишкову вершину F₀. Після приведення маємо ПУДДР (див. рис. 8).

 

Рис. 6	Рис. 7	Рис. 8

 

Бачимо, що у приведеній ДДР є кінцева вершина, що має позначку «1», отже, формула F має моделі, тобто не є суперечною. Таким чином, можна зробити висновок, що подана сукупність тверджень є сумісною.

 

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

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

2. Як перевірити сумісність сукупності тверджень методом Девіса й Патнема?

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

4. Як використати нормальні форми логіки висловлень для перевірки сумісності сукупності тверджень?

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

Поделиться: