Редактирование: Семантическая таблица

В теории доказательства семантическая таблица (/t æ ˈ B L oʊ , ˈ t æ B L oʊ / ; множественное число: таблицы, также названные 'деревом правды') является процедурой решения для сентенциальных и связанных логик и процедурой доказательства для формул логики первого порядка . Аналитическая таблица-древовидная структура, вычисленная для логической формулы, имеющей в каждом узле подформулу исходной формулы, которая будет доказана или опровергнута. Вычисление создает это дерево и использует его для доказательства или опровержения всей Формулы. Метод tableau может также определить выполнимость конечных множеств формул различных логик. Самая популярная процедура по доказательства для модальных логик (Girle 2000). 
[[Файл:Дежавюмок.JPG|300px|thumb|left|Графическое представление частично построенной пропозициональной таблицы]]

==Введение==

Для таблиц опровержения цель состоит в том, чтобы показать, что отрицание формулы не может быть выполнено. Существуют правила обращения с каждым из обычных соединительных слов, начиная с основного соединительного. Во многих случаях применение этих правил приводит к разделению подтаблицы на две части. Создаются экземпляры кванторов. Если какая-либо ветвь таблицы приводит к очевидному противоречию , ветвь закрывается . Если все ветви близки, доказательство полно, и исходная формула является логической истиной .

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

Более конкретно, исчисление таблицы состоит из конечного набора правил, каждое из которых определяет, как разбить одно логическое соединение на его составные части. Правила обычно выражаются в терминах конечных наборов формул, хотя существуют логики, для которых мы должны использовать более сложные структуры данных , такие как мультимножества , списки или даже деревья формул. Отныне " set " обозначает любое из {set, multiset, list, tree}.

Если есть такое правило для каждого логического Связного, то процедура в конечном счете произведет набор, который состоит только из атомарных формул и их отрицания, которые не могут быть разбиты дальше. Такой набор легко распознать как выполнимый или невыполнимый по отношению к семантике рассматриваемой логики. Чтобы отслеживать этот процесс, узлы самой таблицы задаются в виде дерева, а ветви этого дерева создаются и оцениваются систематическим образом. Такой систематический метод поиска по этому дереву дает начало алгоритму выполнения дедукции и автоматизированного рассуждения. Обратите внимание, что это большее дерево присутствует независимо от того, содержат ли узлы наборы, мультимножества, списки или деревья.
==Пропозициональная логика==

В этом разделе представлено исчисление таблиц для классической логики высказываний. Таблица проверяет, является ли данный набор формул выполнимым или нет. Его можно использовать для проверки правильности или следствия: формула действительна, если ее отрицание неосуществимо, а Формулы A 1 , … , A n ldots, A_{n}подразумевают B  Б { A 1 , … , A n , ¬ B } , что она неосуществима.

Основной принцип пропозициональных таблиц состоит в попытке "разбить" сложные формулы на более мелкие до тех пор, пока не будут получены комплементарные пары литералов или дальнейшее расширение невозможно.

Метод работает на дереве, узлы которого помечены формулами. На каждом шаге это дерево изменяется; в пропозициональном случае единственными разрешенными изменениями являются добавления узла как потомка листа. Процедура начинается с генерации дерева, состоящего из цепочки всех формул в наборе, чтобы доказать неудовлетворительность. Вариант к этому стартовому шагу должен начаться с дерева единственного узла, корень которого помечен ⊤  \верхний ; в этом втором случае процедура может всегда копировать формулу в наборе ниже листа. В качестве примера выполнения показана таблица для набора { ( a ∨ ¬ b ) ∧ b , ¬ a } 

Принцип таблицы заключается в том, что формулы в узлах одной ветви рассматриваются совместно, а различные ветви считаются дизъюнктивными. В результате таблица является древовидным представлением формулы, которая является дизъюнкцией соединений. Эта формула эквивалентна множеству, чтобы доказать неудовлетворительность. Процедура изменяет таблицу таким образом, что формула, представленная результирующей таблицей, эквивалентна исходной. Одно из этих соединений может содержать пару комплементарных литералов, и в этом случае это соединение оказывается неудовлетворительным. Если все соединения оказываются неосуществимыми, то исходный набор формул неосуществим.
===И ===
[[Файл:Пропозтцмок.JPG|200px|thumb|left|(a⋁b)⋀b генерирует a⋁b и b]]

Всякий раз, когда ветвь таблицы содержит формулу A ∧ B  A\клин B, которая является соединением двух формул, эти две формулы являются следствиями этой формулы. Этот факт может быть формализован следующим правилом для расширения таблицы:

*    ( ∧  Если ветвь таблицы содержит соединительную формулу A ∧ B , добавьте к ее листу цепь из двух узлов, содержащих формулы A  Одини B  Б

Это правило обычно пишется следующим образом:

*    '''( ∧ ) A ∧ B A B''' 

Вариант этого правила позволяет узлу содержать набор формул, а не одну. В этом случае формулы в этом наборе рассматриваются совместно, поэтому можно добавить { A , B } в конце ветви, содержащей '''A ∧ B''' . Точнее, если узел на ветке помечен X ∪ { A ∧ B } , можно добавить к ветке новый лист '''X ∪ { A , B }''' .

===Или ===
[[Файл:Дупльмок.JPG|200px|thumb|right|a⋁b генерирует A и b]]

Если ветвь таблицы содержит формулу, являющуюся дизъюнкцией двух формул, например '''A ∨ B''' , то можно применить следующее правило:

*    ( ∨  Если узел на ветви содержит дизъюнктивную формулу '''A ∨ B''' , то создайте двух дочерних элементов к листу ветви, содержащих формулы A  Одини B { Б, соответственно.

Это правило разбивает ветвь на две части, различаясь только для конечного узла. Поскольку ветви рассматриваются в дизъюнкции друг к другу, две результирующие ветви эквивалентны исходной, так как дизъюнкция их не общих узлов точно '''A ∨ B''' . Правило для дизъюнкции обычно формально пишется, используя символ |  |для разделения формул двух различных узлов, которые будут созданы:

*    '''( ∨ ) A ∨ B A | B''' 

Если предполагается, что узлы содержат наборы формул , это правило заменяется следующим: если узел помечен Y ∪ { A ∨ B } , к листу ветви, в которой находится этот узел, могут быть присоединены два дочерних узла, помеченных Y ∪ { A } {\displaystyle Y\cup \{A\}} Y\cup \{A\}и Y ∪ { B } , соответственно.

===Не===

Цель таблиц состоит в том, чтобы генерировать все более простые формулы до тех пор, пока не будут созданы пары противоположных литералов или не будет применено никакое другое правило. Отрицание может быть обработано, первоначально делая формулы в нормальной форме отрицания, так, чтобы отрицание только произошло перед литералами. Альтернативно, можно использовать законы де Моргана во время расширения таблицы, так что, например ¬ ( A ∧ B ) , рассматривается как ¬ A ∨ ¬ B . Правила, которые вводят или удаляют пару отрицаний (например, in ¬ ¬ A , также используются в этом случае (в противном случае не было бы возможности расширить формулу, например ¬ ¬ ( A ∧ B ) 

*    ( ¬ 1 ) A ¬ ¬ A 

*    ( ¬ 2 ) ¬ ¬ A A 

===Закрытие===
[[Файл:Тлтормок.JPG|200px|thumb|left|Картина закрыта]]

Каждая таблица может рассматриваться как графическое представление формулы, эквивалентное множеству, из которого построена таблица. Эта формула выглядит следующим образом: каждая ветвь таблицы представляет соединение своих формул; таблица представляет дизъюнкцию своих ветвей. Правила расширения преобразуют таблицу в таблицу, имеющую эквивалентную представленную формулу. Поскольку таблица инициализируется как единая ветвь, содержащая формулы входного множества, все последующие таблицы, полученные из нее, представляют формулы, эквивалентные этому множеству (в варианте, где начальная таблица является единственным узлом, обозначенным true, формулы, представленные таблицами, являются следствиями исходного множества.)
Таблица для выполнимого множества {A⋀c, A⋁b}: все правила были применены к каждой формуле на каждой ветви, но таблица не закрыта (только левая ветвь закрыта), как ожидалось для выполнимых множеств
[[Файл:Закрытмок.JPG|200px|thumb|right|Таблица для выполнимого множества {A⋀c, A⋁b}: все правила были применены к каждой формуле на каждой ветви, но таблица не закрыта (только левая ветвь закрыта), как ожидалось для выполнимых множеств]]

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

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

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

===Таблица с меткой набора===

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

Правила расширения таблицы теперь могут работать на листах таблицы, игнорируя все внутренние узлы. Для соединения правило основано на эквивалентности множества, содержащего соединение A ∧ B с множеством, содержащим оба A } Бвместо него. В частности, если лист помечен '''X ∪ { A ∧ B }''' }меткой, к нему можно добавить узел с меткой '''X ∪ { A , B }''' 

*    '''( ∧ ) X ∪ { A ∧ B } X ∪ { A , B }''' 

Для дизъюнкции множество '''X ∪ { A ∨ B }''' }эквивалентно дизъюнкции двух множеств X ∪ { A }  В результате, если первый набор помечает лист, к нему можно добавить два дочерних элемента, помеченных двумя последними формулами.

*    '''( ∨ ) X ∪ { A ∨ B } X ∪ { A } | X ∪ { B }''' 

Наконец, если набор содержит как литерал, так и его отрицание, эта ветвь может быть закрыта:

*    '''( i d ) X ∪ { p , ¬ p } c l o s e d''' 
Таблица для данного конечного множества X является конечным (перевернутым) деревом с корнем X, в котором все дочерние узлы получены, применяя правила таблицы к их родителям. Ветвь в такой таблице закрыта, если ее конечный узел содержит "закрыто". Таблица закрывается, если все ее ветви закрыты. Таблица открыта, если хотя бы одна ветвь не закрыта.

Вот две закрытые таблицы для множества '''X = { R 0 & ~ r 0, p 0 & ((~ p 0 ∨ q 0) & ~ q 0)} с''' каждым приложением правила, отмеченным с правой стороны (&и ~ стенд для ∧ и ¬ отрицательный , соответственно) 

  {r0 & ~r0, p0 & ((~p0 v q0) & ~q0)} {r0 & ~r0, p0 & ((~p0 v q0) & ~q0)}
 --------------------------------------(&)  ------------------------------------------------------------(&)
 {r0, ~r0, p0 & ((~p0 v q0) & ~q0)} {r0 & ~r0, p0, ((~p0 v q0) & ~q0)}
 -------------------------------------(идентификатор)     - ---------------------------------------------------------(&)
 закрытый {r0 & ~r0, p0, (~P0 v q0), ~q0} 
 -------------------------------------------------------------(в)
 {r0 & ~r0, p0, ~p0, ~q0} / {r0 & ~r0, P0, q0, ~q0}
 -------------------------- (id) ---------------------- (id)
 закрыто закрыто

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

Трех правил ( ∧ )   ( ∨ ) (\ВЭ )и ( i d )  (идентификатор)приведенных выше достаточно, чтобы решить, является ли данный набор X ′  X'формул в отрицательной нормальной форме совместно выполнимым:

*    Просто применяйте все возможные правила во всех возможных ордерах, пока мы не найдем закрытую таблицу X ′  X'или пока мы не исчерпаем все возможности и не придем к выводу, что каждая таблица X ′  X'открыта.

В первом случае X ′  X'совместно невыполнимо, а во втором случае листовой узел открытой ветви дает назначение атомным формулам и отрицаемым атомным формулам, что делает X ′ {\displaystyle X'} X'совместно выполнимым. Классическая логика на самом деле обладает довольно приятным свойством, что нам нужно исследовать только (любую) одну таблицу полностью: если она закрывается X ′  X', то невыполнима, а если она открыта X ′  X', то выполнима. Но это свойство обычно не пользуются другими логиками.

Этих правил достаточно для всей классической логики, взяв начальный набор формул X и заменив каждый член C его логически эквивалентной отрицательной нормальной формой C', дающей набор формул X' . Мы знаем, что X выполнимо тогда и только тогда, когда X' выполнимо, поэтому достаточно искать закрытую таблицу для X', используя описанную выше процедуру.

Установив '''X = { ¬ A }''' }, мы можем проверить, является ли формула a тавтологией классической логики:

*    Если таблица для { ¬ A } }закрывается, то ¬ A neg Aявляется неудовлетворительной, и поэтому A является тавтологией, поскольку никакое присвоение значений истины никогда не сделает ложным. В противном случае любой открытый лист любой открытой ветви любой открытой таблицы for { ¬ A } {\displaystyle \{\neg A\}} \{\neg A\}дает задание, которое фальсифицирует A .

===Условный===

Классическая пропозициональная логика обычно имеет соединительную связь для обозначения материального импликации . Если записать эту связность как⇒, то формула A ⇒ B обозначает " если a, то B ". Можно дать правило таблицы для разбиения ⇒ B на составляющие его формулы. Точно так же мы можем дать по одному правилу для разбиения каждого из '''( A ∧ B )''', ( A ∨ B ), ( A) и '''( A ⇒ B )'''. Вместе эти правила дали бы завершающую процедуру для решения, является ли данный набор формул одновременно выполнимым в классической логике, поскольку каждое правило разбивает одну формулу на составляющие, но ни одно правило не строит большие формулы из меньших составляющих. Таким образом, мы должны в конечном итоге достичь узла, который содержит только атомы и отрицания атомов. Если этот последний узел соответствует (id), то мы можем закрыть ветку, иначе она останется открытой.

Но обратите внимание, что следующие эквивалентности выполняются в классической логике, где (...) = (...) означает, что формула левой стороны логически эквивалентна формуле правой стороны:

'''¬ ( A ∧ B ) = ¬ A ∨ ¬ B 

'''¬ ( A ∨ B ) = ¬ A ∧ ¬ B  

'''¬( ¬ A ) = A ¬ 

'''( A ⇒ B ) = A ∧ 

'''¬ B A ⇒ B = ¬ A ∨ B 

'''A ⇔ B = ( A ∧ B ) ∨ ( ¬ A ∧ ¬ B ) 

'''¬ ( A ⇔ B ) = ( A ∧ ¬ B ) ∨ ( ¬ A ∧ B )''' 

Если мы начнем с произвольной формулы c классической логики и применим эти эквивалентности повторно, чтобы заменить левые стороны на правые стороны в C, то мы получим формулу C', которая логически эквивалентна C, но которая имеет свойство, что C' не содержит никаких последствий и появляется только перед атомарными формулами. Говорят, что такая формула находится в отрицательной нормальной форме, и можно формально доказать, что каждая формула c классической логики имеет логически эквивалентную формулу C' в отрицательной нормальной форме. То есть, C выполним тогда и только тогда, когда c' выполним.

==Логическая таблица первого порядка==

Таблицы расширены до логики предикатов первого порядка двумя правилами для работы с универсальными и экзистенциальными кванторами соответственно. Два различных набора правил могут использоваться; оба используют форму Skolemization для обработки экзистенциальных кванторов, но отличаются на обработке универсальных кванторов.

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

===Таблица первого порядка без объединения===

Формула первого порядка '''∀ x . γ ( x )''' (x)подразумевает все формулы γ ( t ) ), где t  tявляется основным термином. Поэтому следующее правило вывода является правильным:

*    '''( ∀ ) ∀ x . γ ( x ) γ ( t )'''  где t  t произвольный основной термин

В отличие от правил для пропозициональных связок, может потребоваться многократное применение этого правила к одной и той же формуле. В качестве примера, Набор '''{ ¬ P ( a ) ∨ ¬ P ( b ) , ∀ x . P ( x ) }''' }может быть доказан только неудовлетворительным, если оба P ( a ) )и P ( b )  P(b)генерируются '''∀ x . P ( x )''' 
Экзистенциальные кванторы рассматриваются посредством Сколемизации. В частности , формула с ведущим экзистенциальным квантором типа ∃ x . δ ( x )  (x)генерирует свою Сколемизацию δ ( c ) ), где c {\displaystyle c} снаходится новый постоянный символ.

*    ( '''∃ ) ∃ x . δ ( x ) δ ( c )'''  где c } сновый постоянный символ

[[Файл:Первоемок.JPG|400px|thumb|left|Таблица без объединения для {∀x.P (x), ∃x.(P(x)⋁p(f (x))))}. Для ясности формулы нумеруются слева, а формула и правило, используемые на каждом шаге, справа]]

Термин Skolem c  сявляется константой (функцией arity 0), потому что квантификация over x иксне происходит в рамках какого-либо универсального квантора. Если исходная формула содержала некоторые универсальные кванторы, так что количественная x  иксоценка была в пределах их сферы действия, то эти кванторы, очевидно, были удалены путем применения правила для универсальных кванторов.

Правило для экзистенциальных кванторов вводит новые постоянные символы. Эти символы могут использоваться правилом для универсальных кванторов, так что '''∀ y . γ ( y''' )они могут генерировать '''γ ( c )''' , даже если c  сне было в исходной формуле, но является константой Skolem, созданной правилом для экзистенциальных кванторов.

Вышеприведенные два правила для универсальных и экзистенциальных кванторов верны, так же как и пропозициональные правила: если набор формул порождает замкнутую таблицу, этот набор неосуществим. Полнота также может быть доказана: если набор формул неосуществим, существует замкнутая таблица, построенная из него по этим правилам. Однако на самом деле для нахождения такой закрытой таблицы требуется соответствующая политика применения правил. В противном случае, неудовлетворительный набор может генерировать бесконечно растущую таблицу. В качестве примера, Набор { '''¬ P ( f ( c ) ) , ∀ x . P ( x ) }''' } является неудовлетворительным , но замкнутая таблица никогда не получается, если неразумно продолжать применять правило для универсальных кванторов '''∀ x . P ( x )''' , например, генерировать '''P ( c ) , P ( f ( c ) ) , P ( f ( f ( c ) ) )''' , … ldots . Закрытая таблица всегда может быть найдена, исключив эту и подобную "несправедливую" политику применения правил таблицы.

Правило для универсальных кванторов ( ∀ ) forall ) является единственным недетерминированным правилом, так как оно не указывает, с каким термином создавать экземпляр. Кроме того, в то время как другие правила должны применяться только один раз для каждой формулы и каждого пути, в котором формула находится, это может потребовать нескольких приложений. Однако применение этого правила может быть ограничено отсрочкой применения правила до тех пор, пока не будет применено какое-либо другое правило, и ограничением применения правила обоснованными терминами, которые уже появляются на пути таблицы. Приведенный ниже вариант таблиц с унификацией направлен на решение проблемы недетерминизма.

===Таблица первого порядка с объединением===

Основная проблема таблицы без унификации заключается в том, как выбрать основной термин t } tдля универсального правила квантора. Действительно, можно использовать все возможные основные термины, но очевидно, что большинство из них могут быть бесполезны для закрытия таблицы.

Решение этой проблемы заключается в том, чтобы" отложить " выбор термина до того момента, когда следствие правила позволит закрыть хотя бы одну ветвь таблицы. Это может быть сделано с помощью переменной вместо термина, так что '''∀ x''' . γ ( x ) гамма (x)генерирует '''γ ( x ′ )''' , а затем позволяет замены для последующей замены x ′  x'термином. Правило для универсальных кванторов становится:

*    '''( ∀ ) ∀ x . γ ( x ) γ ( x ′ )'''  где x ′  x'переменная не встречается везде в таблице

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

[[Файл:Обьединмок.JPG|400px|thumb|left|Таблица первого порядка с объединением для {∀x.P (x), ∃x.(P(x)⋁p(f (x))))}. Для ясности формулы нумеруются слева, а формула и правило, используемые на каждом шаге, справа]]

Это правило использует переменную вместо основного термина. Выгода этого изменения заключается в том, что этим переменным может быть дано значение, когда ветвь таблицы может быть закрыта, решая проблему генерации терминов, которые могут быть бесполезны.

*    '''( σ )'''  	если σ sigma } \сигма является наиболее общим объединителем двух литералов A  Одини B  Б, где A  Одини отрицание B  Бпроисходит в той же ветви таблицы, σ сигма может быть применено одновременно ко всем формулам таблицы 

В качестве примера { ¬ P ( a ) , ∀ x . P ( x ) }можно доказать неудовлетворимость путем первого генерирования P ( x 1 ) ; отрицание этого литерала унифицируется с ¬ P ( a ) {\displaystyle \neg P(a)} \neg P (a)наиболее общим объединителем, являющимся заменой, которая заменяет x 1  a  a} один; применение этой замены приводит к замене P ( x 1 ) , которая закрывает таблицу.

Это правило закрывает хотя бы ветвь таблицы-ту, которая содержит рассматриваемую пару литералов. Однако замена должна быть применена ко всей таблице, а не только к этим двум литералам. Это выражается в том, что свободные переменные таблицы являются жесткими : если вхождение переменной заменяется чем-то другим, все остальные вхождения той же переменной должны быть заменены таким же образом. Формально, свободные переменные (неявно) универсально квантифицированы, и все формулы таблицы находятся в пределах этих кванторов.

Экзистенциальные кванторы имеют дело со Сколемизацией. В отличие от таблицы без объединения, термины Skolem могут быть не просто постоянными. Действительно, формулы в таблице с унификацией могут содержать свободные переменные, которые неявно считаются универсально квантифицированными. В результате такая формула '''∃ x . δ ( x )''' )может находиться в пределах универсальных кванторов; если это так, то термин Сколема не является простой константой, а членом, состоящим из нового символа функции и свободных переменных формулы.

*    '''( ∃ ) ∃ x . δ ( x ) δ ( f ( x 1 , … , x n ) )''' 

Это правило включает упрощение по правилу, где x 1 , … , x n ldots, x_{n}свободные переменные ветви, не δ delta } дельта одного. Это правило может быть дополнительно упрощено путем повторного использования символа функции, если он уже использовался в Формуле, идентичной δ дельта переименованию переменных.

Формула, представленная таблицей, получена способом, который подобен пропозициональному случаю с дополнительным предположением, что свободные переменные считаются универсально квантифицированными. Что касается пропозиционального случая, формулы в каждой ветви соединены, а полученные формулы разъединены. Кроме того, все свободные переменные результирующей формулы универсально количественно определены. Все эти кванторы имеют всю формулу в своем объеме. Другими словами, если '''F  Ф''' формула получена путем разъединения соединения формул в каждой ветви и x 1 , … , x n ldots, x_{n}являются свободными переменными в ней, то '''∀ x 1 , … , x n . F .Ф''' формула представлена таблицей. Применяются следующие соображения:

*    Предположение, что свободные переменные универсально количественно, - это то , что делает применение наиболее общего объединителя разумным правилом: поскольку γ ( x ′ )    гамма (x')означает, что γ gamma } \гамма это верно для каждого возможного значения x ′  x', то γ ( t ) \gamma (t)верно для термина t {\displaystyle t} t, который заменяет наиболее общий объединитель x  икс.
*    Свободные переменные в таблице жестки: все вхождения одной и той же переменной должны быть заменены одним и тем же членом. Каждая переменная может считаться символом, представляющим термин, который еще предстоит решить. Это является следствием того, что свободные переменные предполагаются универсально количественно по всей Формуле, представленной таблицей: если одна и та же переменная происходит бесплатно в двух разных узлах, оба вхождения находятся в области одного и того же квантификатора. В качестве примера, если формулы в двух узлах A ( x )  Икс)и B ( x )  B (x)где x  икссвободны в обоих, формула, представленная таблицей, является чем-то в виде ∀ x . ( . . . A ( x ) . . . B ( x ) . . . ) ..B (x)...). Эта формула подразумевает, что '''( . . . A ( x ) . . . B ( x ) . . . )'''  '''(...A(x)...B(x)...)} (...Икс.)..B (x)...)'''истинна для любого значения x икс, но не вообще подразумевает '''( . . . A ( t ) . . . A ( t ′ ) . . . )  (...A(t)...A(t')...)} (...A (t)...A (t')...)'''для двух различных терминов t  Т', поскольку эти два термина могут вообще принимать разные значения. Это означает, что x  иксне может быть заменено двумя различными терминами '''В A ( x )'''  Икс)и B ( x ) .
*    Свободные переменные в Формуле для проверки достоверности также считаются универсально количественными. Однако эти переменные не могут быть оставлены свободными при построении таблицы, потому что правила таблицы работают на обратном формуле, но все же рассматривают свободные переменные как универсально квантифицированные. Например, '''P ( x ) → P ( c )''' )недопустимо (неверно не в модели где '''D = { 1 , 2 } , P ( 1 ) = ⊥ , P ( 2 ) = ⊤ , c = 1 , ,''' а в интерпретации где x = 2 . Следовательно, { P ( x ) , ¬ P ( c ) } }выполнимо (удовлетворяется той же моделью и интерпретацией). Однако замкнутая таблица может быть сгенерирована с '''P ( x )''' помощью '''and ¬ P ( c )''' )и заменой x  с будет генерировать закрытие. Правильная процедура состоит в том, чтобы сначала сделать универсальные кванторы явными, тем самым генерируя '''∀ x . ( P ( x ) → P ( c ) )''' 

Следующие два варианта также верны.

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

Таблицы с унификацией могут быть доказаны полными: если набор формул неосуществим, он имеет доказательство таблицы с унификацией. Однако на самом деле найти такое доказательство может быть трудной проблемой. В отличие от случая без объединения, применение замены может изменить существующую часть таблицы; в то время как применение замены закрывает по крайней мере ветвь, это может сделать другие ветви невозможными закрыть (даже если набор невыполним).

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

Проблема, что некоторые таблицы, которые могут быть произведены, невозможно закрыть, даже если набор невыполним, характерна для других наборов правил расширения таблицы: даже если некоторые определенные последовательности применения этих правил позволяют построить закрытую таблицу (если набор невыполним), некоторые другие последовательности приводят к таблицам, которые не могут быть закрыты. Общие решения для этих случаев описаны в разделе" Поиск таблицы".

==Исчисления таблицы и их свойства==

Исчисление таблицы-это набор правил, который позволяет строить и изменять таблицы. Пропозициональные правила таблицы, правила таблицы без унификации и правила таблицы с унификацией-все это исчисления таблицы. Некоторые важные свойства, которыми может обладать или не обладать табличное исчисление, - это полнота, разрушительность и доказательство слияния.

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

Замечательное различие между таблицей с объединением и другими двумя исчислениями состоит в том, что последние два исчисления только изменяют таблицу, добавляя к ней новые узлы, в то время как первый позволяет заменам изменять существующую часть таблицы. В более общем плане исчисления таблицы классифицируются как деструктивные или неразрушающие в зависимости от того, добавляют ли они только новые узлы к таблице или нет. Таким образом, таблица с объединением разрушительна, в то время как пропозициональная таблица и таблица без объединения не разрушительны.

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

Исчисление таблицы-это просто набор правил, которые говорят, как таблица может быть изменена. Процедура доказательства-это метод фактического нахождения доказательства (если оно существует). Другими словами, исчисление таблиц-это набор правил, а процедура доказательства-это политика применения этих правил. Даже если исчисление завершено, не каждый возможный выбор применения правил приводит к доказательству неудовлетворительного множества. Например, '''{ P ( f ( x ) ) , R ( c ) , ¬ P ( f ( c ) ) ∨ ¬ R ( c ) , ∀ x . Q ( x ) }'''  является неудовлетворительным, но обе таблицы с объединением и таблицы без объединения позволяют правилу для универсальных кванторов применяться повторно к последней формуле, в то время как простое применение правила для дизъюнкции к третьей напрямую приведет к закрытию.

Для процедур доказывания дано определение полноты: процедура доказывания является строго полной, если она позволяет найти замкнутую таблицу для любого данного неудовлетворительного набора формул. Доказательство слияния основного исчисления имеет отношение к полноте: доказательство слияния является гарантией того, что замкнутая таблица всегда может быть сгенерирована из произвольной частично построенной таблицы (если множество неосуществимо). Без доказательства слияния, применение "неправильного" правила может привести к невозможности сделать таблицу полной, применяя другие правила.

Пропозициональные таблицы и таблицы без объединения имеют строго полные процедуры доказательства. В частности, полная процедура доказывания заключается в справедливом применении правил. Это связано с тем, что единственный способ, которым такие исчисления не могут генерировать замкнутую таблицу из неудовлетворительного набора, - это не применять некоторые применимые правила.

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

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

Если исчисление таблицы закончено, каждый невыполнимый набор формул имеет связанную замкнутую таблицу. Хотя эта таблица всегда может быть получена путем применения некоторых правил исчисления, проблема, какие правила применять для данной формулы все еще остается. В результате, полнота не подразумевает автоматически существование осуществимой политики применения правил, которая всегда приводит к закрытой таблице для каждого данного неудовлетворительного набора формул. Хотя справедливая процедура доказательства завершена для ground tableau и tableau без объединения, это не относится к таблице с объединением. 

[[Файл:Рправтлмок.JPG|600px|thumb|centre|Дерево поиска в пространстве таблиц для {∀x.P (x), P(c)⋁Q(c), ∃y.Q (c)}. Для простоты формулы множества были опущены из всех таблиц на рисунке и прямоугольника, используемого вместо них. Закрытая таблица находится в жирном поле; другие ветви могут быть расширены.]]

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

Поскольку каждая ветвь может быть бесконечной, это дерево должно быть посещено вширь, а не в глубину. Это требует большого пространства, так как ширина дерева может расти экспоненциально. Метод, который может посещать некоторые узлы более одного раза, но работает в полиномиальном пространстве, заключается в посещении глубины с итеративным углублением: сначала вы посещаете дерево до определенной глубины, затем увеличиваете глубину и выполняете посещение снова. Эта конкретная процедура использует глубину (которая также является числом правил таблицы, которые были применены) для принятия решения, когда остановиться на каждом шаге. Вместо этого использовались различные другие параметры (например, размер таблицы, обозначающей узел).
===Сокращение поиска===

Размер дерева поиска зависит от количества (дочерних) таблиц, которые могут быть созданы из данной (родительской) таблицы. Таким образом, сокращение числа таких таблиц сокращает требуемый поиск.

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

Различные методы сокращения поиска запрещают создание некоторых таблиц на том основании, что закрытая таблица все еще может быть найдена путем расширения других. Эти ограничения называются глобальными. В качестве примера глобального ограничения можно использовать правило, которое определяет, какая из открытых ветвей должна быть расширена. В результате, если таблица имеет, например, две незамкнутые ветви, правило указывает, какая из них должна быть расширена, запрещая расширение второй. Это ограничение уменьшает пространство поиска, так как один из возможных вариантов теперь запрещен; однако полнота не пострадает, так как вторая ветвь все равно будет расширена, если первая в конечном итоге будет закрыта. Например, таблица с корнем ¬ a ∧ ¬ b , дочерним a ∨ b  b и двумя листьями a  один b  бможет быть закрыта двумя способами: ( ∧ ) wedge )} (\клин )сначала к a один, а затем к b  б, или наоборот. Очевидно, что нет необходимости следовать обоим вариантам; можно рассматривать только тот случай, в котором ( ∧ ) wedge )} (\клин )он был впервые применен a  один, и игнорировать тот случай, в котором он был впервые применен b  б. Это глобальное ограничение, потому что то, что позволяет пренебречь этим вторым расширением, - это наличие другой таблицы, где расширение применяется к a } одинпервому и второму расширению b  б впоследствии.

==Таблицы клаузул==

В применении к наборам предложений (а не к произвольным формулам) методы таблиц позволяют повысить эффективность. Предложение первого порядка-это формула '''∀ x 1 , … , x n L 1 ∨ ⋯ ∨ L m''' , которая не содержит свободных переменных и каждая L i из которых является литералом. Универсальные кванторы часто опущены для ясности, так что, например '''P ( x , y ) ∨ Q ( f ( x )''' ) ), фактически означает '''∀ x , y . P ( x , y ) ∨ Q ( f ( x ) )''' . Обратите внимание, что, если понимать буквально, эти две формулы не совпадают с выполнимыми: скорее, выполнимость '''P ( x , y ) ∨ Q ( f ( x ) )''' )такая же, как и у '''∃ x , y . P ( x , y ) ∨ Q ( f ( x ) )'''  \существует x, y.P (x,y)\vee Q (f (x)). То, что свободные переменные универсально количественно определены, не является следствием определения выполнимости первого порядка; это скорее используется в качестве неявного общего предположения при работе с предложениями.

Единственными правилами расширения, которые применимы к предложению, являются ( ∀ ) )и ( ∨ ) ; эти два правила могут быть заменены их комбинацией без потери полноты. В частности, следующее правило соответствует последовательному применению правил ( ∀ ) } (\forall )и ( ∨ )  (\ВЭ )исчисления первого порядка с унификацией.

*    '''( C ) L 1 ∨ ⋯ ∨ L n L 1 ′ | ⋯ | L n ′'''  где '''L 1 ′ ∨ ⋯ ∨ L n ′ }''''получается путем замены каждой переменной на новую в '''L 1 ∨ ⋯ ∨ L n''' 

Когда набор, который будет проверен на выполнимость, только составлен из предложений, это и правила объединения достаточны, чтобы доказать невыполнимость. В других мирах, таблицы исчислений состоит из ( C ) и ( σ )sigma )} (сигма)является полным.

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

*    '''( C ) L 1 ∨ ⋯ ∨ L n L 1 ′ | ⋯ | L n ′'''   где '''L 1 ′ ∨ ⋯ ∨ L n''' ′ 'получается путем замены каждой переменной на новую in L 1 ∨ ⋯ ∨ L n , которая является предложением входного набора

Поскольку это правило напрямую использует предложения во входном наборе, нет необходимости инициализировать таблицу в цепочку входных предложений. Поэтому исходную таблицу можно инициализировать с помощью одного узла с меткой t r u e true} истинный; эта метка часто опускается как неявная. В результате этого дальнейшего упрощения каждый узел таблицы (кроме корня) помечается литералом.

Для таблицы предложений можно использовать ряд оптимизаций. Эта оптимизация направлена на сокращение числа возможных таблиц, которые необходимо изучить при поиске замкнутой таблицы, как описано в разделе "Поиск замкнутой таблицы" выше.
===Таблица соединений===

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

сильная связанность
*    при развертывании ветви используйте предложение input только в том случае, если оно содержит литерал, который можно объединить с отрицанием литерала в текущем листе
слабая связанность
*    разрешить использование предложений, содержащих литерал, объединяющийся с отрицанием литерала в ветке

Оба условия применимы только к ветвям, состоящим не только из корня. Второе определение допускает использование предложения, содержащего литерал, который объединяется с отрицанием литерала в ветви, в то время как первое только дополнительное ограничение, что литерал должен быть в листе текущей ветви.

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

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

Это можно увидеть на следующем (пропозициональном) примере. Таблица, составленная из цепочки t r u e − a  правда-адля набора предложений '''{ a , ¬ a ∨ b , ¬ c ∨ d , ¬ b }''' , может быть в общем случае расширена с использованием каждого из четырех предложений ввода, но соединение позволяет использовать только расширение ¬ a ∨ b . Это означает, что дерево таблиц имеет четыре листа в целом, но только один, если наложена связность. Это означает, что связность оставляет только одну таблицу, чтобы попытаться расширить, а не четыре, чтобы рассмотреть в целом. Несмотря на это сокращение выбора, теорема полноты подразумевает, что замкнутая таблица может быть найдена, если множество невыполнимо.

Условия связности при применении к пропозициональному (клаузальному) случаю делают результирующее исчисление неконфлюентным. В качестве примера, { a , b , ¬ b } }является неудовлетворительным, но применение ( C ) к a  одингенерирует цепь t r u e − a  правда-а, который не закрыт и к которому никакое другое правило расширения не может быть применено без нарушения или сильной или слабой связности. В случае слабой связности слияние выполняется при условии, что предложение, используемое для расширения корня, имеет отношение к неудовлетворительности, то есть оно содержится в минимально неудовлетворительном подмножестве набора предложений. К сожалению, проблема проверки соответствия предложения этому условию сама по себе является трудной проблемой. Несмотря на отсутствие слияния, замкнутая таблица может быть найдена с помощью поиска, как представлено в разделе "Поиск замкнутой таблицы" выше. В то время как поиск сделан необходимым, связанность уменьшает возможные варианты расширения, таким образом делая поиск более эффективным.
===Регулярные таблицы===

Таблица регулярна, если литерал не встречается дважды в одной ветви. Соблюдение этого условия позволяет уменьшить возможные варианты расширения таблицы, поскольку предложения, которые произвели бы нерегулярную таблицу, не могут быть расширены.

Однако эти запрещенные шаги расширения бесполезны. Если B  Бявляется ветвью, содержащей литерал L Л, и C  Сявляется предложением, расширение которого нарушает регулярность, то C  Ссодержит L  Л. Чтобы закрыть таблицу, нужно расширить и закрыть, среди прочего, ветвь , где B − L  B-L, где L  Лпроисходит дважды. Однако формулы в этой ветви точно такие же, как формулы B  Бв одиночку. В результате те же шаги расширения, которые закрываются B − L  B-L, также закрываются B  Б. Это означает, что расширение C  Сбыло ненужным; более того, если C  С содержащийся в других литералах, его расширение произвело другие листья, которые должны были быть закрыты. В пропозициональном случае расширение, необходимое для закрытия этих листьев, совершенно бесполезно; в случае первого порядка они могут влиять только на остальную часть таблицы из-за некоторых унификаций; однако они могут быть объединены с заменами, используемыми для закрытия остальной части таблицы.
==Таблицы для модальных логик==

В модальной логике модель содержит набор возможных миров, каждый из которых связан с оценкой истинности; отношение доступности говорит, когда мир доступен от другого. Модальная формула может указывать не только условия над возможным миром, но и на те, которые доступны из него. В качестве примера, ◻ A  \Box Aверно в мире, если A  Одинверно во всех мирах, которые доступны из него.

Что касается пропозициональной логики, то таблицы модальной логики основаны на рекурсивном разбиении формул на ее основные компоненты. Расширение модальной формулы может, однако, потребовать указания условий в разных мирах. В качестве примера, если ¬ ◻ A Box Aистинно в мире, то существует мир, доступный из него, где A  Одинложно. Однако к пропозициональным нельзя просто добавить следующее правило.

*    '''¬ ◻ A ¬ A''' 

В пропозициональных таблицах все формулы относятся к одной и той же оценке истинности, но предварительное условие вышеприведенного правила выполняется в мире, а следствие-в другом. Не принимая во внимание это приведет к неправильным результатам. Например, формула a ∧ ¬ ◻ a neg Box a} a\wedge \neg Box aутверждает, что a  одинистинна в текущем мире и a  a} одинложна в мире, доступном из него. Просто применяя ( ∧ ) (\клин )и правило расширения выше будет производить a одини ¬ a neg a но эти две формулы не должны вообще порождать противоречия , как это происходит в разных мирах. Модальные таблицы исчислений содержат правила типа одного выше, но включают механизмы, чтобы избежать неправильного взаимодействия формул, относящихся к различным мирам.

Технически, таблицы для модальных логик проверяют выполнимость набора формул: они проверяют, существует ли модель M  М и мир w  Вт, так что формулы в наборе верны в этой модели и мире. В приведенном выше примере, в то время a  одинкак говорится об истинности a одинin w  Вт, формула ¬ ◻ a Box aутверждает истину ¬ a neg aв некотором мире w ′  ч -, который доступен w  Вти который может в целом отличаться от w Вт. Табличные вычисления для модальной логики учитывают, что формулы могут относиться к различным мирам.

Этот факт имеет важное значение: формулы, которые существуют в мире, могут подразумевать условия над различными преемниками этого мира. Неудовлетворительность может тогда быть доказана из подмножества формул, относящихся к единственному преемнику. Это справедливо, если мир может иметь более одного преемника, что верно для большинства модальных логик. Если это так, то формула like ¬ ◻ A ∧ ¬ ◻ B Box B истинна, если существует преемник, где ¬ A neg A удерживает, и существует преемник, где ¬ B neg B удерживает. С другой стороны, если можно показать неудовлетворительность ¬ A neg A в произвольном преемнике, формула оказывается неудовлетворительной без проверки миров, где ¬ B B зацепки. В то же время , если можно показать неудовлетворительность ¬ B  нет необходимости проверять ¬ A B, одного из этих двух способов всегда достаточно, чтобы доказать неудовлетворительность, если формула неудовлетворительна. Например,можно расширить таблицу, рассматривая произвольный мир, где ¬ A  \neg A выполняется. Если это расширение приводит к неудовлетворительности, то исходная формула оказывается неудовлетворительной. Однако также возможно, что неудовлетворительность не может быть доказана таким образом, и что мир, где ¬ B neg B вместо этого должны были быть рассмотрены удержания. В результате всегда можно доказать неудовлетворительность, расширяясь или ¬ ◻ A  Aтолько или ¬ ◻ B  Bтолько; Однако, если неправильный выбор сделан, результирующая таблица не может быть закрыта. Расширение любой подформулы приводит к табличным исчислениям, которые являются полными, но не доказательными. Поэтому может потребоваться поиск, как описано в разделе "Поиск замкнутой таблицы".

В зависимости от того, относятся ли предварительное условие и следствие правила расширения таблицы к одному и тому же миру или нет, правило называется статическим или транзакционным. В то время как правила для пропозициональных связок все статичны, не все правила для модальных связок являются транзакционными: например, в каждой модальной логике , включая аксиому T, это ◻ A  A подразумевает '''A'''  Одинв том же самом мире. В результате относительное (модальное) правило расширения таблицы статично, поскольку и его предварительное условие, и следствие относятся к одному и тому же миру.
===Формула-удаление таблицы===

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

В качестве примера, в S5 каждая формула ◻ A  истинная в мире, также истинна во всех доступных мирах (то есть во всех доступных мирах A  Одини ◻ A  \Box A истинны). Поэтому, применяя ¬ ◻ A ¬ A a}{\neg A}}, чье следствие имеет место в другом мире, человек удаляет все формулы из ветви, но может сохранить все формулы ◻ A  как они имеют место и в новом мире. Чтобы сохранить полноту, удаленные формулы затем добавляются ко всем другим ветвям, которые все еще относятся к старому миру.
===Мир-маркированная таблица===

Другой механизм обеспечения правильного взаимодействия между формулами, относящимися к разным мирам , заключается в переходе от формул к Меченым формулам: вместо того, чтобы писать A  Один, можно было бы написать '''w : A  w: A''', чтобы сделать его явным, что '''A'''  Одинимеет место в мире w {\displaystyle w} Вт.

Все пропозициональные правила расширения приспособлены к этому варианту, заявляя, что все они относятся к формулам с той же самой мировой этикеткой. Например, w : A ∧ B {\displaystyle w:A\wedge B} w:A\wedge Bгенерирует два узла с меткой w : A {\displaystyle w:A} w: Aand w : B ; ветвь закрывается только в том случае, если она содержит два противоположных литерала одного и того же мира, например w : a  w: aand w : ¬ a ; замыкание не генерируется, если две метки мира различны, например in w : a  w: aand w ′ : ¬ a 
Модальное правило расширения может иметь последствия, которые относятся к другим мирам. Например, правило for ¬ ◻ A  '''A''' будет записано следующим образом

*    '''w : ¬ ◻ A w ′ : ¬ A''' 

Предпосылка и следствие этого правила относятся к мирам w  В ти w ′  ч -, соответственно. Различные исчисления используют различные методы для отслеживания доступности миров, используемых в качестве меток. Некоторые из них включают псевдо-формулы, как w R w ′  wRw'обозначить, что w ′  ч -доступно w  Вт. Некоторые другие используют последовательности целых чисел в качестве мировых меток, эта нотация неявно представляет отношение доступности (например, '''( 1 , 4 , 2 , 3 )  (1,4,2,3)} (1,4,2,3''')доступна '''( 1 , 4 , 2 )(1,4,2)} (1,4,2)).)'''
===Таблицы меток набора===

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

Таблицы для модальных логик используются для проверки выполнимости набора модальных формул в данной модальной логике. Учитывая набор формул S  С, они проверяют существование модели M  Ми w  Вт такого мира M , w ⊨ S w\models S} M, w \ models S.

Правила расширения зависят от конкретной используемой модальной логики. Система таблиц для основной модальной логики K может быть получена путем добавления к пропозициональным правилам таблиц следующего:

*    '''( K ) ◻ A 1 ; … ; ◻ A n ; ¬ ◻ B A 1 ; … ; A n ; ¬ B''' 

Интуитивно предпосылка этого правила выражает истинность всех формул A 1 , … , A n ldots, A_{n}во всех доступных мирах и истинность ¬ B neg B} \neg Bв некоторых доступных мирах. Следствием этого правила является формула, которая должна быть истинной в одном из тех миров, где ¬ B neg B} \neg Bона истинна.

Более технически, методы модальных таблиц проверяют существование модели M  Ми мира w  Вт, которые делают набор формул истинным. Если '''◻ A 1 ; … ; ◻ A n ; ¬ ◻ B''' Bони истинны w  Вт, должен быть мир w ′  ч -, который доступен w  Вти который делает A 1 ; … ; A n ; ¬ B  Bистинным. Таким образом, это правило сводится к получению набора формул, которые должны быть выполнены в таких w ′  ч -формулах .

В то время как предварительные '''◻ A 1 ; … ; ◻ A n ; ¬ ◻ B'''  Bусловия предполагаются удовлетворенными M , w M, w, последствия '''A 1 ; … ; A n ; ¬ B'''  Bпредполагаются удовлетворенными в M , w ′  M, w': та же самая модель, но возможно различные миры. Таблицы с метками набора явно не отслеживают мир, где каждая формула считается истинной: два узла могут ссылаться или не ссылаться на один и тот же мир. Однако формулы, обозначающие любой данный узел, предполагаются истинными в том же мире.

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

Примечательно, ( K ) что не распространяется непосредственно на несколько отрицаемых коробочных формул, таких как in '''◻ A 1 ; … ; ◻ A n ; ¬ ◻ B 1 ; ¬ ◻ B 2''' : Хотя существует доступный мир, где B 1 }ложно и один, в котором B 2 ложно, эти два мира не обязательно одинаковы.

В отличие от пропозициональных правил, ( K ) устанавливает условия во всех своих предпосылках. Например, он не может быть применен к узлу, помеченному a ; '''◻ b ; ◻ ( b → c ) ; ¬ ◻ c''' ; хотя этот набор является несогласованным , и это может быть легко доказано путем применения ( K ), это правило не может быть применено из-за формулы a  один, которая даже не относится к несогласованности. Удаление таких формул стало возможным благодаря правилу:

*    '''( θ ) A 1 ; … ; A n ; B 1 ; … ; B m A 1 ; … ; A n''' 

Добавление этого правила (Правило прореживания) делает результирующее исчисление неконфлюентным: таблицу для несогласованного множества может быть невозможно закрыть, даже если существует замкнутая таблица для того же множества.

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

Этого недетерминизма можно избежать, ограничив использование ( θ ) тета )таким образом, что он применяется только перед модальным правилом расширения и удаляет только формулы, которые делают это другое правило неприменимым. Это условие также может быть сформулировано путем объединения двух правил в одно. Полученное правило дает тот же результат, что и старое, но неявно отбрасывает все формулы, которые сделали старое правило неприменимым. ( θ ) тета )Доказано, что этот механизм удаления сохраняет полноту для многих модальных логик.

Аксиома Т выражает рефлексивность отношения доступности: каждый мир доступен сам по себе. Соответствующее правило расширения таблицы:

*    '''( T ) A 1 ; … ; A n ; ◻ B A 1 ; … ; A n ; ◻ B ; B''' 

Это правило связывает условия над одним и тем же миром: если ◻ B  Bистинно в мире, то рефлексивность B  Бтакже истинна и в том же мире . Это правило статично, а не транзакционно, поскольку и его предварительное условие, и последующее относятся к одному и тому же миру.

Это правило копируется ◻ B  B из предварительного условия в последующее, несмотря на то, что эта формула была "использована" для генерации B  Б. Это правильно, так как рассматриваемый мир один и тот же, то ◻ B  B и держится там. Это "копирование" необходимо в некоторых случаях. Например, необходимо доказать несогласованность ◻ '''( a ∧ ¬ ◻ a )'''  a): единственные применимые правила-это порядок '''( T ) , ( ∧ ) , ( θ ) , ( K )''' , из которого один блокируется, если ◻ a  a не копируется.
===Вспомогательные таблицы===

Другой метод для того, чтобы иметь дело с формулами, держащимися в альтернативных мирах, должен начать различную таблицу для каждого нового мира, который введен в таблицу. Например, ¬ ◻ A  A подразумевает, что A  Одинложно в доступном мире, таким образом, каждый начинает новую таблицу, укорененную ¬ A . Эта новая таблица присоединена к узлу исходной таблицы, где было применено правило расширения; закрытие этой таблицы немедленно генерирует закрытие всех ветвей, где тот узел, независимо от того, связан ли тот же самый узел с другими вспомогательными таблицами. Правила расширения для вспомогательных таблиц такие же, как и для исходной таблицы; поэтому вспомогательная таблица может иметь в свою очередь другие (суб-)вспомогательные таблицы.
===Глобальные предположения===

Приведенные выше модальные таблицы устанавливают согласованность набора формул и могут быть использованы для решения задачи локального логического следствия. Это проблема определения того , истинна ли для каждой модели '''M'''  М, если A  Одинона истинна в мире w  Вт, то B  Бтакже истинна и в том же мире. Это то же самое, что проверка истинности B Бв мире модели, в предположении, что '''A'''  Одинэто также верно в том же мире той же модели.

Связанная с этим проблема является глобальной проблемой следствия, где предполагается, что формула (или набор формул) '''G'''  Гверна во всех возможных мирах модели. Проблема в том, чтобы проверить, верно ли во всех моделях '''M'''  М, где '''G'''  Гверно во всех мирах, '''B'''  Бтакже верно во всех мирах.

Локальные и глобальные предположения различаются на моделях, где предполагаемая формула верна в некоторых мирах, но не в других. В качестве примера, { P , ¬ ◻ ( P ∧ Q ) } влечет ¬ ◻ '''Q'''  Q за собой глобально, но не локально. Локальное вовлечение не имеет места в модели, состоящей из двух миров, делающих '''P  Pи ¬ P , Q  P, Q''' истинных соответственно, и где второе доступно из первого; в первом мире предположение верно, но ◻ Q } \Box Qложно. Этот контрпример работает, потому P  P что можно считать истинным в мире и ложным в другом. Если, однако, то же предположение считается глобальным, '''¬ P''' P не допускается ни в одном мире модели.

Эти две проблемы могут быть объединены, так что можно проверить, является ли B  Блокальным следствием A  Одинглобального предположения '''G'''  Г. Табличные исчисления могут иметь дело с глобальным предположением по правилу, позволяющему добавлять его к каждому узлу, независимо от мира, к которому он относится.

==Обозначение==

Иногда используются следующие соглашения.
===Однородная нотация===

При написании правил расширения таблиц формулы часто обозначаются с использованием соглашения, так что, например α alpha } \альфа , всегда считается α 1 ∧ α 2 . В следующей таблице приведены обозначения формул в логике высказываний, первого порядка и модальности. 

[[Файл:Таблмок.JPG|400px|thumb|left|описание]]

Каждая метка в первом столбце считается формулой в других столбцах. Наложенная формула, такая как α 1 ¯ указывает, что α 1 }является отрицанием любой формулы, появляющейся на ее месте, так что, например, в Формуле ¬ ( a ∨ b ) )подформула α 1 }является отрицанием a один.

Так как каждая метка указывает много эквивалентных формул, эта нотация позволяет написать одно правило для всех этих эквивалентных формул. Например, правило расширения связи формулируется как:

*    '''( α ) α α 1 α 2 '''

===Подписанные формулы===

Формула в таблице принимается истинной. Подписанные таблицы позволяют утверждать, что формула ложна. Обычно это достигается добавлением метки к каждой формуле, где метка t указывает формулы, предполагаемые истинными, а F-предполагаемые ложными. Другое, но эквивалентное обозначение состоит в том, чтобы написать формулы, которые считаются истинными слева от узла, а Формулы предполагаются ложными справа от него.
==История==

Метод семантических таблиц был изобретен голландским логиком Эвертом Виллемом бетом (Beth 1955) и упрощен для классической логики Раймондом Смулляном (Smullyan 1968, 1995). Это упрощение Смулляна," односторонние картины", описанные выше. Метод смулляна был обобщен на произвольные многозначные пропозициональные логики и логики первого порядка Вальтером Карниелли (Carnielli 1987). таблицы можно интуитивно рассматривать как последовательные системы в обратном порядке. Эта симметричная связь между таблицами и последовательными системами была официально установлена в (Carnielli 1991).
==См. также==

*    [[Разрешение (логика)]]
==Пруф==
[https://www.irit.fr/Lotrec/ .irit.fr/Lotrec/]
* [https://www.umsu.de/logik/trees/ .umsu.de/logik/trees/]
* [http://hackage.haskell.org/package/tableaux hackage.haskell.org/package/tableaux]
* [https://www.springer.com/computer/theoretical+computer+science/journal/10817 .springer.com/computer/theoretical+computer+science/journal/10817]
* [http://www.tableaux-ar.org/ .tableaux-ar.org/]



[[Категория:Логика]]