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

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

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. Як використати нормальні форми логіки висловлень для перевірки сумісності сукупності тверджень?

СПИСОК ВИКОРИСТАНОЇ ТА РЕКОМЕНДОВАНОЇ ЛІТЕРАТУРИ

1. Мендельсон Э. Введение в математическую логику. – М.: Наука, 1984. – 320 с.

2. Столл Р. Множества. Логика. Аксиоматические теории. – М.: Просвещение, 1968. – 231 с.

3. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. – М.: Наука, 1983. – 360 с.

4. Bryant R.E. Graph-based algorithms for Boolean function manipulation // IEEE Transactions on Computers, 8 (C-35), 1986. – P. 677-691.

Скорочення, символи та позначення

ДДР – двійкова діаграма рішень

ДНФ (днф) – диз’юнктивна нормальна форма

КНФ (кнф) – кон’юнктивна нормальна форма

нфр – нормальна форма розгалуження

ПУДДР – приведена упорядкована двійкова діаграма рішень

УДДР – упорядкована двійкова діаграма рішень

 – заперечення

 – імплікація

 – диз’юнкція

 – кон’юнкція

 – еквівалентність

F₁,F₂,…,F_n╞═ F – формула F є логічним наслідком формул F₁,F₂,…,F_n

F₁ = F₂ – формули F₁ та F₂ приймають однакові істинносні значення при

кожній інтерпретації

 – порожній диз’юнкт

FF₁,F₀ – розгалуження із перевірним виразом F та гілками F₁ та F₀

ПРЕДМЕТНИЙ ПОКАЖЧИК

Атом 3 Вивід порожнього диз’юнкту 25 Гілка розгалуження 29 Двійкова діаграма рішень 31 – упорядкована 31 – приведена 32 Диз’юнкт 13 – одиничний 13 – порожній 13 – тавтологічний 14 – r-літерний 13 Диз’юнкція 3 Еквівалентність 4 Заперечення 3 Імплікація 3 Інтерпретація формули 9 Контрарна пара 13 Контрарні літери 13 Кон’юнкт 14 Кон’юнкція 3 Літера 13 – негативна 13 – позитивна 13 – чиста у множині диз’юнктів 23 Логічна зв’язка 3 Логічне слідування 17 Тавтологія 10 Формула 4 – атомарна 3 – істинна при даній інтерпретації 9 – тотожно істинна 10 – тотожно хибна 10 – хибна при даній інтерпретації 9

Логічний наслідок 17 Множина диз’юнктів 14 Мова логіки висловлень 4 Модель формули 9 Наддиз’юнкт 26 Нормальна форма формули – диз’юнктивна 14 – кон’юнктивна 13 – розгалуження 29 Оператор розгалуження 29 Перевірний вираз 29 Піддиз’юнкт 26 Правило – однолітерних диз’юнктів 22 – резолюції 24 – розщеплення 23 – тавтології 22 – чистих літер 23 Резольвента 24 Рівносильність 3 Розгалуження 29 Стратегія – викреслювання 26 – вхідної резолюції 27 – одиничної резолюції 28 Суперечність 10 Формули – еквівалентні 12 – рівносильні 12