Метод двійкових діаграм рішень

Нехай F, F₀, F₁ – формули. Розгалуженням називається вираз виду FF₁,F₀, який визначається так: FF₁,F₀=(FF₁)(FF₀). Формула F називається перевірним виразом,  – оператором розгалуження, F₁,F₀ – гілками розгалуження. Будемо називати розгалуження формулою.

З наведеного означення випливає, що логічні зв’язки , , , ,  можуть бути виражені через оператор розгалуження й логічні константи 0 та 1 таким чином, що: а) перевірні вирази є атомами, б) атоми зустрічаються лише у перевірних виразах. Дійсно, маємо: Р=(Р0,1); PQ=P(Q1,0),0; РQ=P(Q1,0),(Q0,1); PQ=P1,(Q1,0); PQ=P(Q1,0),1. Зазначимо також, що кожна формула F може бути записана у вигляді F1,0.

Формула F є у нормальній формі розгалуження (нфр), якщо F побудована лише з атомів, операторів розгалуження й логічних констант 0 та 1, перевірними виразами є атоми, атоми зустрічаються лише як перевірні вирази.

Наприклад, формула P(Q0,(R0,1)),(R(P1,0),(Q1,0)) є у нфр, а формули (РQ)R,0 та Р(RQ),(QP) – ні.

Позначимо F[0/P] (F[1/P]) формулу, що є результатом заміни у формулі F атома Р на 0 (1). Тоді формулу F, що містить атом Р, можна подати у вигляді F=РF[1/P],F[0/P]. Користуючись цим співвідношенням, можна кожну формулу привести до нфр. Нехай, наприклад, F=(PQ)(QR). Тоді F[1/P]= =(1Q)(QR)=Q(QR), F[0/P]=(0Q)(QR)=QR. F=P(Q(QR)), (QR). Виконуючи далі підстановки 1 та 0 замість атома Q, маємо:

F=Q(P(1(1R)),(1R)),(P(0(0R)),(0R))=Q(P0,1),PR,R.

Оскільки R=R1,0, то маємо: F=Q(P0,1),(P(R1,0),(R1,0)).

Двійковою діаграмою рішень (ДДР) називається ациклічний кореневий позначений орграф, у якому є одна чи дві кінцеві вершини (тобто вершини, степінь виходу яких дорівнює нулю), що мають (різні) позначки 0 або 1, степінь виходу некінцевих вершин дорівнює двом, на множині некінцевих вершин визначено функції var, low, high такі, що коли u – некінцева вершина, то її позначкою є var(u), а (u, low(u)) та (u, high(u)) – дуги, інцидентні вершині u. Областю значень функції var є деяка множина позначок, область значень функцій high, low – множина вершин ДДР.

Двійкова діаграма рішень називається упорядкованою (УДДР), якщо для усіх її шляхів зберігається один і той самий лінійний порядок позначок некінцевих вершин. Двійкова діаграма рішень (упорядкована або ні) називається приведеною (П(У)ДДР), якщо для усіх її некінцевих вершин u, v виконується: (var(u)=var(v))(low(u)=low(v))(high(u)=high(v))u=v й low(u)high(u).

Визначимо рекурсивну процедуру побудови формули F^u, що визначається вершиною u деякої ПУДДР. Кінцева вершина визначає логічну константу, некінцева вершина u з позначкою Р визначає розгалуження, перевірним виразом якого є Р, а суміжні вершини визначають гілки розгалуження, тобто F⁰=0, F¹=1, F^u=var(u)F^high(u),F^low(u).

За формулою у нфр очевидним чином можна побудувати дерево, яке після ототожнення однакових підвиразів перетворюється на ДДР. На рис.1 зображено УДДР для логічної константи 1. Ця діаграма не є приведеною, вона містить дві надлишкові вершини, що відповідають перевірним виразам. Діаграма на рис.2 є УДДР для формули х₁х₃ з однією надлишковою вершиною. Дуги виду (u,high(u)) зображено суцільними лініями, дуги виду (u,low(u)) – пунктирними.

Теорема 4. Для будь-якої формули F(A₁,…,A_n) логіки висловлень існує єдина ПУДДР з упорядкуванням позначок A₁…A_n, така що для кореневої вершини u F^u=F.

Н

Рис. 2

аведені результати забезпечують такий спосіб перевірки тавтологічності (суперечності) формули логіки висловлень. Побудуємо для даної формули F її нормальну форму розгалуження, вибравши певний порядок атомів (це можна зробити для будь-якої формули логіки висловлень). Потім за нфр побудуємо УДДР, при потребі здійснивши її приведення. Якщо результатом є діаграма, що складається з однієї кінцевої вершини, яка має позначку 1 (0), то формула F є тавтологією (суперечністю). Якщо побудована ПУДДР має некінцеві вершини, то формула F не є ні тавтологією, ні суперечністю, але має моделі.

Розглянемо формулу (х₁y₁)(x₂y₂). Зафіксуємо порядок атомів: x₁<y₁<x₂<y₂. На рис.3 зображено ПУДДР даної формули. Діаграма показує, що формула не є тавтологією й не є суперечністю. За допомогою цієї діаграми можна побудувати моделі формули, наприклад, х₁=y₁=1, х₂=y₂=0.

Рис. 1	Рис. 2	Рис. 3

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

Розглянемо приклади використання описаних вище методів для перевірки логічної правильності міркування.