Правила образования деревьев в логике высказываний

П1. Если формула имеет видлф, тогда дерево, в которое она входит, начинается или продолжается в каждой своей ветви формулой ф.

П2. Если формула имеет вид (ф & <�р), тогда дерево, в которое она входит, начинается или продолжается в каждой своей ветви формулами фи (р(коммутативность и идемпотентность формул фи (р подразумевается):

ПЗ. Если формула имеет вид (ф v <�р), тогда дерево, в которое она входит, начинается или продолжается разветвлением на формулу ф и на формулу <�р(коммутативность и идемпотентность формул фи (рподразумевается):

П4. Если формула имеет вид (ф э (р), тогда дерево, в которое она входит, начинается или продолжается разветвлением на формулуiф и формулу <�р:

П5. Если формула имеет вид (ф = <�р), тогда дерево, в которое она входит, начинается или продолжается ветвлением на формулы (0 & (р) и (—1 ф & —1 (р)'.

П6. Если формула имеет вид (ф * (р), тогда дерево, в которое она входит, начинается или продолжается разветвлением на формулу (ф & -1 <�р) и формулу (-1 ф & <�р):

П7. Если формула имеет вид ->(ф & <�р), тогда дерево, в которое она входит, начинается или продолжается разветвлением на формулулф и формулу -п (р:

П8. Если формула имеет видп(ф v <�р), тогда дерево, в которое она входит, начинается или продолжается в каждой своей ветви формулами -пф и -iqr.

П9. Если формула имеет видi (0 э (р), тогда дерево, в которое она входит, начинается или продолжается в каждой своей ветви формулами -10 ИI (рг.

П10. Если от общей вершины, включающей формулу 0, исходят две ветви с формулами 0 и (р, тогда обе эти ветви удаляются и дерево продолжается формулой 0.

П11. Если имеется пара ветвей вида 0 и (0 & <�р), тогда для продолжения дерева остается только ветвь с формулой 0.

П12. Если имеется пара ветвей типа (0 & (р) и (0 & -i.

П13. Если есть пара ветвей типа ф и (-10 & (р), тогда для продолжения дерева остаются ветви с формулами ф и (р.

П14. Ветвь, содержащая по крайней мере одну пару противоречащих друг другу формул (не обязательно атомарных), называется замкнутой, отмечается знаком? и не подлежит дальнейшему продолжению. После своей идентификации замкнутая ветвь может быть удалена.

П15. Процесс конструирования дерева формулы начинается с представления подформул, соединяемых главным логическим союзом формулы, и продолжается до тех пор, пока все ее подформулы не будут представлены в виде ветвей дерева, содержащих только атомарные формулы или их отрицания.

Каждая ветвь правильно построенного дерева эквивалентна конъюнкции всех атомарных формул и/или их отрицаний, содержащихся в ней. Назовем такую ветвь полной. Каждое дерево эквивалентно дизъюнкции всех своих полных ветвей.

Процесс конструирования дерева формулы завершается одним из следующих возможных результатов:

• 1. Если дерево формулы включает хотя бы две ветви с нулевой вершиной (без формул), одна из которых содержит атомарную формулу, а другая — ее отрицание, значит, исходная формула — логическая истина.
• 2. Если все ветви дерева формулы замкнуты, значит, исходная формула — логическая ложь.
• 3. Если хотя бы одна ветвь дерева формулы не замкнута и нет ни одной пары ветвей с нулевой вершиной, одна из которых содержит атомарную формулу, а другая — ее отрицание, значит, исходная формула — логически нейтральная.

Пример 1. Построить дерево формулы.

(((Л э В) & (СvЛ)) э (Л => (В & С))).

Для большей ясности процесс конструирования в этом и следующих двух примерах разделен на отдельные этапы с указанием справа в скобках правил, на основании которых совершены преобразования.

Дерево анализируемой формулы содержит две ветви с нулевой вершиной и с формулами В и ->В, логически отрицающими друг друга. Значит, эта формула — логическая истина.

Пример 2. Построит^ дерево формулы.

Все ветви дерева анализируемой формулы замкнуты. Значит, она — логическая ложь.

Пример 3. Построить дерево формулы.

((—Л v В) & (—1 В v С v —Л)).

Дерево анализируемой формулы содержит две незамкнутые ветви. Хотя обе они имеют нулевую вершину, но не состоят из формул, логически отрицающих друг друга. Значит, данная формула — логически нейтральная.