Cтраница 2
Определение 6.4. Назовем покрытие семантической таблицы устойчивым, если расщепление входящих в него вершин не приводит к появлению новых запрещенных фигур. [16]
Предположим, что в семантической таблице Т число вершин не превосходит числа ветвей. Присоединим к концу одной из ветвей Т некоторую атомарную семантическую таблицу. [17]
Таким образом, в семантических таблицах ветвление обозначает дизъюнкцию, а последовательное соединение - конъюнкцию утверждений. [18]
Ветви 2 и я4 этой семантической таблицы противоречивы. [19]
К концу каждой непротиворечивой ветви семантической таблицы Тп мы присоединяем атомарную семантическую таблицу, имеющую корнем X. При этом вершина X становится особой вершиной. [20]
Тогда V согласовано с некоторой ветвью семантической таблицы. [21]
Метод аналитических таблиц ( или метод семантических таблиц, или метод Хинтикка) является эффективной процедурой доказательства теорем, как для логики высказываний, так и для логики предикатов первого порядка. Но если метод резолюции работает с формулами, представленными в КНФ, то метод аналитических таблиц оперирует с формулами, представленными в ДНФ. Вывод осуществляется на бинарных деревьях, вершины которых отмечены формулами, причем вершина называется концевой, если она не имеет потомков, простой, если она имеет только одного потомка и дизъюнктивной, если она имеет двух потомков. Каждая ветвь дерева представлена конъюнкцией формул, а само дерево - дизъюнкцией своих ветвей. [22]
Поясним описанную методику на примере построения противоречивой семантической таблицы. [23]
Если бы мы поместили в корень семантической таблицы утверждения о том, что закон Пирса истинен, то заключение осталось бы таким же. [24]
Лемма, очевидно, верна для атомарных семантических таблиц. [25]
Первый из описанных методов алгоритмического доказательства использует семантические таблицы. Используя теорию доказательств Бет и Хинтикка в 1955 г. построили алгоритм, устанавливающий, является высказывание тавтологией или нет. [26]
Прежде, чем определить общие правила построения семантических таблиц, рассмотрим пример. [27]
Теперь мы сформулируем понятия, необходимые для построения семантических таблиц. [28]
ЗСТ может иметь бесконечное число вершин, тогда как семантические таблицы для PL всегда конечны. [29]
В замечании 2.8.11 мы упоминали о том, что семантические таблицы и замкнутые систематические таблицы являются деревьями. По лемме Кенига ( лемма 1.11.9) каждое конечно ветвящееся дерево с бесконечным числом вершин имеет по крайней мере одну бесконечную ветвь. [30]