Метод аналитических таблиц - Method of analytic tableaux

Графическое представление частично построенной пропозициональной таблицы

В теории доказательств , то семантическая таблица ( / т æ б л oʊ , т æ б л oʊ / , множественное число: Tableaux , называемый также истина дерево ) является процедура принятия решения по сентенциальному и связанному с ними логик, и процедура доказательства для формул логика первого порядка . Аналитическая таблица - это древовидная структура, вычисляемая для логической формулы, имеющая в каждом узле подформулу исходной формулы, которая должна быть доказана или опровергнута. Вычисление строит это дерево и использует его для доказательства или опровержения всей формулы. Табличный метод может также определять выполнимость конечных наборов формул различных логик. Это самая популярная процедура доказательства для модальных логик (Girle 2000).

Вступление

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

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

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

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

Логика высказываний

В этом разделе представлено табличное исчисление для классической логики высказываний. Таблица проверяет, является ли данный набор формул выполнимым или нет. Его можно использовать для проверки либо действительности, либо следствия: формула действительна, если ее отрицание невыполнимо, а формулы подразумевают, если невыполнимо. ${\ displaystyle A_ {1}, \ ldots, A_ {n}}$ ${\ displaystyle B}$ ${\ Displaystyle \ {A_ {1}, \ ldots, A_ {n}, \ neg B \}}$

Главный принцип пропозициональных таблиц - это попытка «разбить» сложные формулы на более мелкие до тех пор, пока не будут созданы дополнительные пары литералов или пока не станет невозможным дальнейшее расширение.

Исходная таблица для {(a⋁¬b) ⋀b, ¬a}

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

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

А также

(a⋁¬b) ⋀b порождает a⋁¬b и b

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

( ) Если ветвь таблицы содержит конъюнктивную формулу , добавьте к ее листу цепочку из двух узлов, содержащих формулы и ${\ Displaystyle \ клин}$ ${\ Displaystyle A \ клин B}$ ${\ displaystyle A}$ ${\ displaystyle B}$

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

{\ displaystyle (\ land) {\ frac {A \ wedge B} {\ begin {array} {c} A \\ B \ end {array}}}}

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

Или же

a⋁¬b порождает a и ¬b

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

( ) Если узел ветки содержит дизъюнктивную формулу , создайте двух дочерних узлов для листа ветви, содержащих формулы и , соответственно. ${\ displaystyle \ vee}$ ${\ displaystyle A \ vee B}$ ${\ displaystyle A}$ ${\ displaystyle B}$

Это правило разделяет ветвь на две, отличаясь только для последнего узла. Поскольку ветви рассматриваются в дизъюнкции друг с другом, две результирующие ветви эквивалентны исходной, поскольку дизъюнкция их необщих узлов точно . Правило дизъюнкции обычно формально записывается с использованием символа для разделения формул двух различных узлов, которые должны быть созданы: ${\ displaystyle A \ vee B}$ ${\ displaystyle |}$

{\ displaystyle (\ vee) {\ гидроразрыва {A \ vee B} {A \ mid B}}}

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

Нет

Цель таблиц - генерировать все более простые формулы до тех пор, пока не будут созданы пары противоположных литералов или пока не будет применяться какое-либо другое правило. Отрицание можно обработать, изначально создав формулы в отрицательной нормальной форме , так что отрицание происходит только перед литералами. В качестве альтернативы можно использовать законы Де Моргана во время расширения таблицы, так что, например , рассматривается как . В этом случае также используются правила, которые вводят или удаляют пару отрицаний (например, in ) (в противном случае не было бы возможности расширить формулу, например : ${\ Displaystyle \ neg (А \ клин В)}$ ${\ displaystyle \ neg A \ vee \ neg B}$ ${\ displaystyle \ neg \ neg A}$ ${\ Displaystyle \ neg \ neg (A \ клин B)}$

{\ Displaystyle (\ neg 1) {\ гидроразрыва {A} {\ neg \ neg A}}}

{\ Displaystyle (\ neg 2) {\ гидроразрыва {\ neg \ neg A} {A}}}

Таблица закрыта

Закрытие

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

Таблица для выполнимого множества {a⋀c, ¬a⋁b}: все правила были применены к каждой формуле в каждой ветви, но таблица не закрыта (закрыта только левая ветвь), как и ожидалось для выполнимых множеств.

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

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

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

Помеченная набором таблица

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

Правила расширения таблицы теперь могут работать на листьях таблицы, игнорируя все внутренние узлы. Для конъюнкции правило основано на эквивалентности набора, содержащего конъюнкцию, с набором, содержащим оба, и вместо него. В частности, если лист помечен значком, к нему можно добавить узел с меткой : ${\ Displaystyle A \ клин B}$ ${\ displaystyle A}$ ${\ displaystyle B}$ ${\ Displaystyle X \ чашка \ {A \ клин B \}}$ ${\ Displaystyle Х \ чашка \ {А, В \}}$

{\ Displaystyle (\ клин) {\ гидроразрыва {Х \ чашка \ {А \ клин В \}} {Х \ чашка \ {А, В \}}}}

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

{\ displaystyle (\ vee) {\ frac {X \ cup \ {A \ vee B \}} {X \ cup \ {A \} | X \ cup \ {B \}}}}

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

{\ displaystyle (id) {\ frac {X \ cup \ {p, \ neg p \}} {closed}}}

Таблица для данного конечного множества X - это конечное (перевернутое) дерево с корнем X, в котором все дочерние узлы получены путем применения правил таблицы к своим родителям. Ветвь в такой таблице закрыта, если ее листовой узел содержит "closed". Таблица закрыта, если все ее ветви закрыты. Таблица открыта, если хотя бы одна ветка не закрыта.

Вот две закрытые таблицы для множества X = { r 0 & ~ r 0, p 0 & ((~ p 0 ∨ q 0) & ~ q 0)} с каждым приложением правила, отмеченным справа (& и ~ обозначают и , соответственно) ${\ Displaystyle \ клин}$ ${\ displaystyle \ neg}$

 {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)}
 -------------------------------------(id)                         ----------------------------------------------------------(&)
            closed                                                      {r0 & ~r0, p0,  (~p0 v q0),  ~q0} 
                                                                -------------------------------------------------------------(v)
                                                                  {r0 & ~r0, p0, ~p0, ~q0}       |   {r0 & ~r0, p0, q0, ~q0}
                                                                 -------------------------- (id)     ----------------------  (id)
                                                                          closed                            closed

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

Три правил , и приведенные выше, то достаточно , чтобы решить , является ли данный набор формул в отрицаются нормальной форма совместно выполним: ${\ Displaystyle (\ клин)}$ ${\ Displaystyle (\ vee)}$ ${\ displaystyle (id)}$ ${\ displaystyle X '}$

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

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

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

Устанавливая мы можем проверить формулу ли является тавтологией классической логики: ${\ Displaystyle X = \ {\ neg A \}}$

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

Условный

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

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

${\ displaystyle {\ begin {array} {lcl} \ neg (A \ land B) & = & \ neg A \ lor \ neg B \\\ neg (A \ lor B) & = & \ neg A \ land \ neg B \\\ neg (\ neg A) & = & A \\\ neg (A \ Rightarrow B) & = & A \ land \ neg B \\ A \ Rightarrow B & = & \ neg A \ lor B \\ A \ Стрелка влево-вправо B & = & (A \ земля B) \ lor (\ neg A \ land \ neg B) \\\ neg (A \ Leftrightarrow B) & = & (A \ land \ neg B) \ lor (\ neg A \ земля B) \ end {array}}}$

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

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

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

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

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

Формула первого порядка подразумевает все формулы, где - основной член . Следовательно, верно следующее правило вывода: ${\ Displaystyle \ forall х. \ гамма (х)}$ ${\ Displaystyle \ гамма (т)}$ ${\ displaystyle t}$

{\ Displaystyle (\ forall) {\ гидроразрыва {\ forall x. \ gamma (x)} {\ gamma (t)}}}

где - произвольный основной член

{\ displaystyle t}

В отличие от правил для пропозициональных связок, может потребоваться многократное применение этого правила к одной и той же формуле. Например, можно доказать , что набор неудовлетворителен только в том случае, если оба и генерируются из . ${\ Displaystyle \ {\ neg P (a) \ vee \ neg P (b), \ forall xP (x) \}}$ ${\ Displaystyle P (а)}$ ${\ Displaystyle P (b)}$ ${\ displaystyle \ forall xP (x)}$

С экзистенциальными квантификаторами обращаются посредством сколемизации. В частности, формула с ведущим экзистенциальным квантификатором, например, генерирует свою сколемизацию , где - новый постоянный символ. ${\ Displaystyle \ существует х. \ дельта (х)}$ ${\ Displaystyle \ дельта (с)}$ ${\ displaystyle c}$

{\ Displaystyle (\ существует) {\ гидроразрыва {\ существует х. \ дельта (х)} {\ дельта (с)}}}

где новый постоянный символ

{\ displaystyle c}

Таблица без объединения для {∀xP (x), ∃x. (¬P (x) ⋁¬P (f (x)))}. Для наглядности формулы слева пронумерованы, а формула и правило, используемые на каждом этапе, - справа.

Термин Сколема является константой (функция арности 0), потому что количественная оценка не происходит в рамках какого-либо универсального квантора. Если исходная формула содержала некоторые универсальные кванторы, такие, что квантификация была в пределах их объема, эти кванторы, очевидно, были удалены путем применения правила для универсальных кванторов. ${\ displaystyle c}$ ${\ displaystyle x}$ ${\ displaystyle x}$

Правило для кванторов существования вводит новые постоянные символы. Эти символы могут использоваться правилом для универсальных квантификаторов, так что они могут генерироваться, даже если они не были в исходной формуле, а являются константой Сколема, созданной правилом для квантификаторов существования. ${\ Displaystyle \ forall y. \ gamma (y)}$ ${\ Displaystyle \ гамма (с)}$ ${\ displaystyle c}$

Вышеупомянутые два правила для универсальных и экзистенциальных кванторов верны, как и правила высказываний: если набор формул порождает замкнутую таблицу, этот набор неудовлетворителен. Полнота также может быть доказана: если набор формул невыполним, существует замкнутая таблица, построенная из него по этим правилам. Однако на самом деле нахождение такой закрытой таблицы требует подходящей политики применения правил. В противном случае неудовлетворительный набор может генерировать бесконечно растущую таблицу. Например, набор неудовлетворителен, но замкнутая таблица никогда не будет получена, если неразумно продолжать применять правило для универсальных кванторов , например, генерировать . Всегда можно найти закрытую таблицу, исключив эту и подобные ей «несправедливые» политики применения правил таблицы. ${\ Displaystyle \ {\ neg P (е (с)), \ forall xP (x) \}}$ ${\ displaystyle \ forall xP (x)}$ ${\ Displaystyle P (C), P (F (C)), P (F (F (C))), \ ldots}$

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

Таблица первого порядка с унификацией

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

Решение этой проблемы состоит в том, чтобы «отложить» выбор термина до того момента, когда консеквент правила позволит закрыть хотя бы ветвь таблицы. Это можно сделать, используя переменную вместо термина, чтобы генерировать , а затем разрешить замену позже заменить термином. Правило для универсальных кванторов становится следующим: ${\ Displaystyle \ forall х. \ гамма (х)}$ ${\ Displaystyle \ гамма (х ')}$ ${\ displaystyle x '}$

{\ Displaystyle (\ forall) {\ гидроразрыва {\ forall x. \ gamma (x)} {\ gamma (x ')}}}

где - переменная, не встречающаяся где-либо еще в таблице

{\ displaystyle x '}

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

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

{\ Displaystyle (\ sigma)}

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

{\ displaystyle \ sigma}

{\ displaystyle A}

{\ displaystyle B}

{\ displaystyle A}

{\ displaystyle B}

{\ displaystyle \ sigma}

Например, может быть доказана неудовлетворительность, сначала сгенерировав ; отрицание этого литерала унифицируемо с , самый общий объединитель - это подстановка, которая заменяет на ; применение этой замены приводит к замене на , что закрывает таблицу. ${\ Displaystyle \ {\ neg P (а), \ forall xP (x) \}}$ ${\ Displaystyle P (x_ {1})}$ ${\ Displaystyle \ neg P (а)}$ ${\ displaystyle x_ {1}}$ ${\ displaystyle a}$ ${\ Displaystyle P (x_ {1})}$ ${\ Displaystyle P (а)}$

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

С экзистенциальными кванторами занимается сколемизация. В отличие от таблицы без унификации, термины Сколема не могут быть просто постоянными. Действительно, формулы в таблице с объединением могут содержать свободные переменные, которые неявно считаются универсально определенными. В результате такая формула может входить в сферу действия универсальных кванторов; в этом случае термин Сколема - это не простая константа, а член, состоящий из нового символа функции и свободных переменных формулы. ${\ Displaystyle \ существует х. \ дельта (х)}$

{\ Displaystyle (\ существует) {\ гидроразрыва {\ существует x. \ delta (x)} {\ delta (f (x_ {1}, \ ldots, x_ {n}))}}}

где - символ новой функции, а свободные переменные

{\ displaystyle f}

{\ displaystyle x_ {1}, \ ldots, x_ {n}}

{\ displaystyle \ delta}

Таблица первого порядка с объединением для {∀xP (x), ∃x. (¬P (x) ⋁¬P (f (x)))}. Для наглядности формулы слева пронумерованы, а формула и правило, используемые на каждом этапе, - справа.

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

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

Предположение, что свободные переменные универсально количественно определены, - вот что делает применение наиболее общего унификатора разумным правилом: поскольку это означает, что это верно для каждого возможного значения , то верно для члена, которым заменяет наиболее общий унификатор . ${\ Displaystyle \ гамма (х ')}$ ${\ displaystyle \ gamma}$ ${\ displaystyle x '}$ ${\ Displaystyle \ гамма (т)}$ ${\ displaystyle t}$ ${\ displaystyle x}$
Свободные переменные в таблице жесткие: все вхождения одной и той же переменной должны быть заменены одним и тем же термином. Каждую переменную можно рассматривать как символ, представляющий термин, который еще не определен. Это является следствием того, что свободные переменные считаются универсально количественными по всей формуле, представленной таблицей: если одна и та же переменная встречается бесплатно в двух разных узлах, оба вхождения находятся в области действия одного и того же квантификатора. Например, если формулы в двух узлах - это и , где свободна в обоих, формула, представленная таблицей, является чем-то в форме . Эта формула подразумевает, что это верно для любого значения , но в целом не подразумевает для двух разных членов и , поскольку эти два члена могут в общем принимать разные значения. Это означает, что нельзя заменить двумя разными терминами в и . ${\ Displaystyle А (х)}$ ${\ Displaystyle В (х)}$ ${\ displaystyle x}$ ${\ Displaystyle \ forall х. (... А (х) ... В (х) ...)}$ ${\ Displaystyle (... А (х) ... В (х) ...)}$ ${\ displaystyle x}$ ${\ Displaystyle (... А (т) ... А (т ') ...)}$ ${\ displaystyle t}$ ${\ displaystyle t '}$ ${\ displaystyle x}$ ${\ Displaystyle А (х)}$ ${\ Displaystyle В (х)}$
Свободные переменные в формуле для проверки достоверности также считаются универсально определенными. Однако эти переменные нельзя оставлять свободными при построении таблицы, потому что правила таблицы работают с обратной формулой, но по-прежнему рассматривают свободные переменные как универсально количественно определяемые. Например, неверно (неверно в модели where и интерпретации where ). Следовательно, выполнимо (удовлетворяется той же моделью и той же интерпретацией). Тем не менее, закрытая таблица может быть сгенерирована с и , и подставив с будет генерировать замыкание. Правильная процедура состоит в том, чтобы сначала сделать универсальные кванторы явными, и таким образом произвести . ${\ Displaystyle P (x) \ rightarrow P (c)}$ ${\ Displaystyle D = \ {1,2 \}, P (1) = \ bot, P (2) = \ top, c = 1}$ ${\ displaystyle x = 2}$ ${\ Displaystyle \ {P (x), \ neg P (c) \}}$ ${\ Displaystyle P (x)}$ ${\ displaystyle \ neg P (c)}$ ${\ displaystyle x}$ ${\ displaystyle c}$ ${\ Displaystyle \ forall x. (P (x) \ rightarrow P (c))}$

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

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

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

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

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

Табличные исчисления и их свойства

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

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

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

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

Процедуры доказательства

Табличное исчисление - это просто набор правил, которые говорят, как можно изменить таблицу. Процедура доказательства - это метод фактического нахождения доказательства (если оно существует). Другими словами, табличное исчисление - это набор правил, а процедура доказательства - это политика применения этих правил. Даже если исчисление является полным, не каждый возможный выбор применения правил приводит к доказательству неудовлетворительного набора. Например, невыполнимо, но и таблицы с объединением, и таблицы без объединения позволяют многократно применять правило универсальных кванторов к последней формуле, в то время как простое применение правила дизъюнкции к третьей напрямую приведет к закрытию. ${\ Displaystyle \ {п (е (с)), р (с), \ отр Р (е (с)) \ ви \ отр (с), \ forall xQ (x) \}}$

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

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

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

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

В поисках закрытой таблицы

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

Дерево поиска в пространстве таблиц для {∀xP (x), ¬P (c) ⋁¬Q (c), ∃yQ (c)}. Для простоты формулы набора опущены во всех таблицах на рисунке, и вместо них используется прямоугольник. Полужирным шрифтом выделена закрытая таблица; другие ветви могут быть расширены.

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

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

Сокращение поиска

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

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

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

Таблицы статей

При применении к наборам предложений (а не к произвольным формулам) табличные методы позволяют повысить эффективность. Предложение первого порядка - это формула , не содержащая свободных переменных, каждая из которых является литералом. Универсальные кванторы часто опускаются для ясности, так что, например, на самом деле означает . Обратите внимание, что, если понимать их буквально, эти две формулы не то же самое, что и для выполнимости: скорее, выполнимость такая же, как у . Универсальная количественная оценка свободных переменных не является следствием определения выполнимости первого порядка; это скорее используется как неявное общее предположение при работе с предложениями. ${\ Displaystyle \ forall x_ {1}, \ ldots, x_ {n} L_ {1} \ vee \ cdots \ vee L_ {m}}$ ${\ displaystyle L_ {i}}$ ${\ Displaystyle Р (х, у) \ vee Q (е (х))}$ ${\ Displaystyle \ forall x, yP (x, y) \ vee Q (f (x))}$ ${\ Displaystyle Р (х, у) \ vee Q (е (х))}$ ${\ Displaystyle \ существует х, yP (x, y) \ vee Q (f (x))}$

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

{\ displaystyle (C) {\ frac {L_ {1} \ vee \ cdots \ vee L_ {n}} {L_ {1} '| \ cdots | L_ {n}'}}}

где получается заменой каждой переменной на новую в

{\ Displaystyle L_ {1} '\ vee \ cdots \ vee L_ {n}'}

{\ Displaystyle L_ {1} \ vee \ cdots \ vee L_ {п}}

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

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

{\ displaystyle (C) {\ frac {L_ {1} \ vee \ cdots \ vee L_ {n}} {L_ {1} '| \ cdots | L_ {n}'}}}

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

{\ Displaystyle L_ {1} '\ vee \ cdots \ vee L_ {n}'}

{\ Displaystyle L_ {1} \ vee \ cdots \ vee L_ {п}}

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

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

Таблица подключений

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

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

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

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

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

Это можно увидеть на следующем (пропозициональном) примере. Таблицу, состоящую из цепочки для набора предложений, можно в общем случае расширить с помощью каждого из четырех предложений ввода, но соединение допускает только расширение, которое использует . Это означает, что дерево таблиц в целом имеет четыре листа, но только один, если наложена связность. Это означает, что связность оставляет только одну таблицу, которую нужно попытаться расширить, вместо четырех, которые нужно рассматривать в целом. Несмотря на это сокращение выбора, из теоремы о полноте следует, что замкнутая таблица может быть найдена, если множество невыполнимо. ${\ displaystyle true-a}$ ${\ displaystyle \ {a, \ neg a \ vee b, \ neg c \ vee d, \ neg b \}}$ ${\ displaystyle \ neg a \ vee b}$

Условия связности, примененные к пропозициональному (клаузальному) случаю, делают результирующее исчисление неконфлюэнтным. Например, невыполнимо, но применение к генерирует цепочку , которая не замкнута и к которой нельзя применить никакое другое правило расширения без нарушения сильной или слабой связности. В случае слабой связности конфлюэнтность сохраняется при условии, что предложение, используемое для расширения корня, относится к неудовлетворительности, то есть содержится в минимально неудовлетворительном подмножестве множества предложений. К сожалению, проблема проверки того, соответствует ли предложение этому условию, сама по себе является сложной проблемой. Несмотря на несовпадение, закрытую таблицу можно найти с помощью поиска, как показано в разделе «Поиск закрытой таблицы» выше. Хотя поиск необходим, связность сокращает возможные варианты расширения, что делает поиск более эффективным. ${\ Displaystyle \ {а, б, \ нег б \}}$ ${\ displaystyle (C)}$ ${\ displaystyle a}$ ${\ displaystyle true-a}$

Регулярные картины

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

Однако эти запрещенные шаги расширения бесполезны. Если это ветвь, содержащая литерал , и предложение, расширение которого нарушает регулярность, то содержит . Чтобы закрыть таблицу, нужно, в том числе, развернуть и закрыть ветку, где , где встречается дважды. Однако формулы в этой ветке точно такие же, как и формулы одной. В результате те же шаги расширения, которые закрываются, также закрываются . Это означает, что в расширении не было необходимости; более того, если он содержал другие литералы, его расширение генерировало другие листья, которые необходимо было закрыть. В пропозициональном случае расширение, необходимое для закрытия этих листьев, совершенно бесполезно; в случае первого порядка они могут влиять только на остальную часть таблицы из-за некоторых унификаций; однако их можно объединить с заменами, используемыми для закрытия остальной части таблицы. ${\ displaystyle B}$ ${\ displaystyle L}$ ${\ displaystyle C}$ ${\ displaystyle C}$ ${\ displaystyle L}$ ${\ displaystyle BL}$ ${\ displaystyle L}$ ${\ displaystyle B}$ ${\ displaystyle BL}$ ${\ displaystyle B}$ ${\ displaystyle C}$ ${\ displaystyle C}$

Таблицы для модальных логик

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

Что касается логики высказываний, таблицы для модальных логик основаны на рекурсивном разбиении формул на их основные компоненты. Однако расширение модальной формулы может потребовать определения условий для разных миров. Например, если в мире истинно, то существует мир, доступный из него, где ложно. Однако нельзя просто добавить к пропозициональным правилам следующее правило. ${\ displaystyle \ neg \ Box A}$ ${\ displaystyle A}$

{\ displaystyle {\ frac {\ neg \ Box A} {\ neg A}}}

В таблицах высказываний все формулы относятся к одной и той же оценке истинности, но предварительное условие правила, приведенного выше, выполняется в одном мире, в то время как следствие сохраняется в другом. Если этого не принять во внимание, это приведет к неверным результатам. Например, формула утверждает, что она истинна в текущем мире и ложна в мире, доступном из него. Простое применение приведенного выше правила расширения приведет к возникновению и , но эти две формулы в общем случае не должны вызывать противоречия, поскольку они имеют место в разных мирах. Исчисления модальных таблиц действительно содержат правила, подобные приведенным выше, но включают механизмы, позволяющие избежать неправильного взаимодействия формул, относящихся к разным мирам. ${\ Displaystyle а \ клин \ neg \ Box а}$ ${\ displaystyle a}$ ${\ displaystyle a}$ ${\ Displaystyle (\ клин)}$ ${\ displaystyle a}$ ${\ displaystyle \ neg a}$

Технически таблицы для модальных логик проверяют выполнимость набора формул: они проверяют, существует ли модель и мир, такие, что формулы в наборе истинны в этой модели и мире. В приведенном выше примере, хотя и утверждает истинность in , формула утверждает истинность некоторого мира , доступного из и который в целом может отличаться от . Табличные исчисления для модальной логики учитывают, что формулы могут относиться к разным мирам. ${\ displaystyle M}$ ${\ displaystyle w}$ ${\ displaystyle a}$ ${\ displaystyle a}$ ${\ displaystyle w}$ ${\ displaystyle \ neg \ Box a}$ ${\ displaystyle \ neg a}$ ${\ displaystyle w '}$ ${\ displaystyle w}$ ${\ displaystyle w}$

Этот факт имеет важное последствие: формулы, которые справедливы в мире, могут подразумевать условия для различных преемников этого мира. Тогда неудовлетворенность может быть доказана с помощью подмножества формул, относящихся к одному преемнику. Это верно, если у мира может быть более одного преемника, что верно для большинства модальных логик. Если это так, формула, например , истинна, если существует преемник, где есть условия, и преемник, где есть условия. И наоборот, если можно показать невыполнимость в произвольном преемнике, формула оказывается невыполнимой без проверки миров, где выполняется. В то же время, если можно показать неудовлетворенность , нет необходимости проверять . В результате, хотя есть два возможных способа расширения , одного из этих двух всегда достаточно, чтобы доказать невыполнимость, если формула невыполнима. Например, можно расширить таблицу, рассматривая произвольный мир, в котором выполняется. Если это расширение приводит к невыполнимости, исходная формула не выполняется. Однако также возможно, что неудовлетворительность не может быть доказана таким образом, и что вместо этого следовало рассмотреть мир, в котором есть условия. В результате всегда можно доказать неудовлетворенность только расширением или только расширением ; однако, если будет сделан неправильный выбор, итоговая таблица не может быть закрыта. Расширение любой из подформул приводит к табличным исчислениям, которые являются полными, но не сливающимися с доказательствами. Поэтому может потребоваться поиск, описанный в разделе «Поиск закрытой таблицы». ${\ Displaystyle \ neg \ Box A \ клин \ neg \ Box B}$ ${\ displaystyle \ neg A}$ ${\ displaystyle \ neg B}$ ${\ displaystyle \ neg A}$ ${\ displaystyle \ neg B}$ ${\ displaystyle \ neg B}$ ${\ displaystyle \ neg A}$ ${\ Displaystyle \ neg \ Box A \ клин \ neg \ Box B}$ ${\ displaystyle \ neg A}$ ${\ displaystyle \ neg B}$ ${\ displaystyle \ neg \ Box A}$ ${\ displaystyle \ neg \ Box B}$

В зависимости от того, относятся ли предусловие и следствие правила раскрытия таблицы к одному и тому же миру или нет, правило называется статическим или транзакционным. В то время как правила для пропозициональных связок статичны, не все правила для модальных связок являются транзакционными: например, в каждой модальной логике, включая аксиому T , выполняется то, что подразумевает в одном и том же мире. В результате правило относительного (модального) раскрытия таблицы статично, поскольку и его предусловие, и следствие относятся к одному и тому же миру. ${\ displaystyle \ Box A}$ ${\ displaystyle A}$

Таблица удаления формулы

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

Например, в S5 каждая формула, которая истинна в мире, также верна во всех доступных мирах (то есть во всех доступных мирах оба и истинны). Следовательно, при применении , последствия которого сохраняются в другом мире, удаляются все формулы из ветви, но можно сохранить все формулы , так как они действуют и в новом мире. Чтобы сохранить полноту, удаленные формулы затем добавляются ко всем другим ветвям, которые все еще относятся к старому миру. ${\ displaystyle \ Box A}$ ${\ displaystyle A}$ ${\ displaystyle \ Box A}$ ${\ displaystyle {\ frac {\ neg \ Box A} {\ neg A}}}$ ${\ displaystyle \ Box A}$

Мировая таблица

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

Все правила пропозиционального расширения адаптированы к этому варианту, утверждая, что все они относятся к формулам с одним и тем же мировым ярлыком. Например, генерирует два узла, помеченных и ; ветвь закрывается только в том случае, если в ней есть два противоположных литерала одного и того же мира, вроде и ; закрытие не создается, если два мировых ярлыка различны, например, в и . ${\ displaystyle w: A \ клин B}$ ${\ displaystyle w: A}$ ${\ displaystyle w: B}$ ${\ displaystyle w: a}$ ${\ displaystyle w: \ neg a}$ ${\ displaystyle w: a}$ ${\ displaystyle w ': \ neg a}$

Правило модального расширения может иметь последствия, относящиеся к другим мирам. Например, правило для будет записано следующим образом ${\ displaystyle \ neg \ Box A}$

{\ displaystyle {\ frac {w: \ neg \ Box A} {w ': \ neg A}}}

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

Таблицы-разметки

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

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

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

{\ displaystyle (K) {\ frac {\ Box A_ {1}; \ ldots; \ Box A_ {n}; \ neg \ Box B} {A_ {1}; \ ldots; A_ {n}; \ neg B }}}

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

С технической точки зрения, методы модальных таблиц проверяют существование модели и мира, которые делают набор формул истинным. Если истинны в , должен быть мир , доступный из которого и который делает правдой. Таким образом, это правило сводится к получению набора формул, которым должны удовлетворять такие формулы . ${\ displaystyle M}$ ${\ displaystyle w}$ ${\ Displaystyle \ Box A_ {1}; \ ldots; \ Box A_ {n}; \ neg \ Box B}$ ${\ displaystyle w}$ ${\ displaystyle w '}$ ${\ displaystyle w}$ ${\ Displaystyle A_ {1}; \ ldots; A_ {n}; \ neg B}$ ${\ displaystyle w '}$

Предполагается, что предварительные условия выполнены , а последствия считаются выполненными в одной и той же модели, но, возможно, в разных мирах. Таблицы с метками наборов явно не отслеживают мир, в котором каждая формула считается истинной: два узла могут относиться или не относиться к одному и тому же миру. Однако формулы, обозначающие любой данный узел, считаются истинными в том же мире. ${\ Displaystyle \ Box A_ {1}; \ ldots; \ Box A_ {n}; \ neg \ Box B}$ ${\ displaystyle M, w}$ ${\ Displaystyle A_ {1}; \ ldots; A_ {n}; \ neg B}$ ${\ displaystyle M, w '}$

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

Примечательно, что он не распространяется напрямую на несколько формул в рамке с отрицанием, например в : хотя существует доступный мир, в котором ложно, а другой - ложно, эти два мира не обязательно являются одинаковыми. ${\ displaystyle (K)}$ ${\ displaystyle \ Box A_ {1}; \ ldots; \ Box A_ {n}; \ neg \ Box B_ {1}; \ neg \ Box B_ {2}}$ ${\ displaystyle B_ {1}}$ ${\ displaystyle B_ {2}}$

В отличие от пропозициональных правил, формулирует условия по всем своим предусловиям. Например, его нельзя применить к узлу с меткой ; хотя этот набор противоречив, и это можно легко доказать путем применения , это правило не может применяться из-за формулы , которая даже не имеет отношения к несогласованности. Удаление таких формул возможно по правилу: ${\ displaystyle (K)}$ ${\ displaystyle a; \ Box b; \ Box (b \ rightarrow c); \ neg \ Box c}$ ${\ displaystyle (K)}$ ${\ displaystyle a}$

{\ displaystyle (\ theta) {\ frac {A_ {1}; \ ldots; A_ {n}; B_ {1}; \ ldots; B_ {m}} {A_ {1}; \ ldots; A_ {n} }}}

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

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

Этого недетерминизма можно избежать, ограничив использование так, чтобы оно применялось только перед правилом модального расширения и чтобы оно удаляло только формулы, которые делают другое правило неприменимым. Это условие также можно сформулировать, объединив два правила в одно. Результирующее правило дает тот же результат, что и старое, но неявно отбрасывает все формулы, которые сделали старое правило неприменимым. Было доказано, что этот механизм удаления сохраняет полноту для многих модальных логик. ${\ Displaystyle (\ тета)}$ ${\ Displaystyle (\ тета)}$

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

{\ displaystyle (T) {\ frac {A_ {1}; \ ldots; A_ {n}; \ Box B} {A_ {1}; \ ldots; A_ {n}; \ Box B; B}}}

Это правило связывает условия в одном и том же мире: если верно в мире, то по рефлексии верно и в том же мире . Это правило является статическим, а не транзакционным, поскольку и его предусловие, и следствие относятся к одному и тому же миру. ${\ displaystyle \ Box B}$ ${\ displaystyle B}$

Это правило копирует предварительное условие в последующее, несмотря на то, что эта формула «использовалась» для генерации . Это правильно, поскольку рассматриваемый мир один и тот же, поэтому и здесь. Это «копирование» необходимо в некоторых случаях. Например, необходимо доказать несоответствие : единственные применимые правила в порядке , из которых одно блокируется, если не копируется. ${\ displaystyle \ Box B}$ ${\ displaystyle B}$ ${\ displaystyle \ Box B}$ ${\ Displaystyle \ Box (а \ клин \ neg \ Box а)}$ ${\ Displaystyle (Т), (\ клин), (\ тета), (К)}$ ${\ displaystyle \ Box a}$

Вспомогательные таблицы

Другой метод работы с формулами, действующими в альтернативных мирах, - это запускать разные таблицы для каждого нового мира, представленного в таблице. Например, подразумевает, что это неверно в доступном мире, поэтому запускается новая таблица, основанная на . Эта новая таблица присоединяется к узлу исходной таблицы, к которой было применено правило раскрытия; закрытие этой таблицы немедленно генерирует закрытие всех ветвей, где находится этот узел, независимо от того, связан ли этот же узел с другими вспомогательными таблицами. Правила раскрытия вспомогательных таблиц такие же, как и для исходной; следовательно, вспомогательная таблица может по очереди иметь другие (под) вспомогательные таблицы. ${\ displaystyle \ neg \ Box A}$ ${\ displaystyle A}$ ${\ displaystyle \ neg A}$

Глобальные предположения

Приведенные выше модальные таблицы устанавливают непротиворечивость набора формул и могут использоваться для решения локальной проблемы логического следствия . Это проблема того , чтобы говорить ли, для каждой модели , если это верно в мире , то это верно и в том же мире. Это то же самое, что проверка истинности в мире модели в предположении, что это также верно в том же мире той же модели. ${\ displaystyle M}$ ${\ displaystyle A}$ ${\ displaystyle w}$ ${\ displaystyle B}$ ${\ displaystyle B}$ ${\ displaystyle A}$

Связанная с этим проблема - проблема глобальных последствий, когда предполагается, что формула (или набор формул) верна во всех возможных мирах модели. Проблема заключается в том, чтобы проверить, верно ли во всех моделях, где истинно во всех мирах, во всех ли мирах. ${\ displaystyle G}$ ${\ displaystyle M}$ ${\ displaystyle G}$ ${\ displaystyle B}$

Локальные и глобальные предположения различаются в моделях, где предполагаемая формула верна в одних мирах, но не верна в других. Например, влечет за собой глобально, но не локально. Локальное следствие не выполняется в модели, состоящей из двух миров, создающих и истинных, соответственно, и где второй доступен из первого; в первом мире предположение верно, но неверно. Этот контрпример работает, потому что его можно считать истинным в одном мире и ложным в другом. Однако, если то же предположение считается глобальным, оно не допускается ни в одном мире модели. ${\ Displaystyle \ {P, \ neg \ Box (P \ клин Q) \}}$ ${\ displaystyle \ neg \ Box Q}$ ${\ displaystyle P}$ ${\ displaystyle \ neg P, Q}$ ${\ displaystyle \ Box Q}$ ${\ displaystyle P}$ ${\ displaystyle \ neg P}$

Эти две проблемы можно объединить, чтобы можно было проверить, является ли это локальным следствием глобального предположения . Табличные исчисления могут иметь дело с глобальным предположением с помощью правила, разрешающего его добавление к каждому узлу, независимо от того, к какому миру оно относится. ${\ displaystyle B}$ ${\ displaystyle A}$ ${\ displaystyle G}$

Обозначения

Иногда используются следующие условные обозначения.

Единое обозначение

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


Обозначение	Формулы
${\ displaystyle \ alpha}$	${\ Displaystyle \ альфа _ {1} \ клин \ альфа _ {2}}$	${\ displaystyle \ neg ({\ overline {\ alpha _ {1}}} \ vee {\ overline {\ alpha _ {2}}})}$	${\ displaystyle \ neg (\ alpha _ {1} \ rightarrow {\ overline {\ alpha _ {2}}})}$
${\ displaystyle \ beta}$	${\ displaystyle \ beta _ {1} \ vee \ beta _ {2}}$	${\ displaystyle {\ overline {\ beta _ {1}}} \ rightarrow \ beta _ {2}}$	${\ displaystyle \ neg ({\ overline {\ beta _ {1}}} \ клин {\ overline {\ beta _ {2}}})}$
${\ displaystyle \ gamma}$	${\ Displaystyle \ forall х \ гамма _ {1} (х)}$	${\ Displaystyle \ Ne \ существует х {\ overline {\ gamma _ {1} (х)}}}$
${\ displaystyle \ delta}$	${\ Displaystyle \ существует х \ дельта _ {1} (х)}$	${\ displaystyle \ neg \ forall x {\ overline {\ delta _ {1} (x)}}}$
${\ displaystyle \ pi}$	${\ displaystyle \ Diamond \ pi _ {1}}$	${\ displaystyle \ neg \ Box {\ overline {\ pi _ {1}}}}$
${\ displaystyle \ upsilon}$	${\ displaystyle \ Box \ upsilon _ {1}}$	${\ displaystyle \ neg \ Diamond {\ overline {\ upsilon _ {1}}}}$

Каждая метка в первом столбце считается формулой в других столбцах. Выделенная выше формула, такая как, указывает на то, что это отрицание любой формулы, встречающейся на ее месте, так что, например, в формуле подформула является отрицанием . ${\ displaystyle {\ overline {\ alpha _ {1}}}}$ ${\ displaystyle \ alpha _ {1}}$ ${\ Displaystyle \ neg (а \ ви б)}$ ${\ displaystyle \ alpha _ {1}}$ ${\ displaystyle a}$

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

{\ displaystyle (\ alpha) {\ frac {\ alpha} {\ begin {array} {c} \ alpha _ {1} \\\ alpha _ {2} \ end {array}}}}

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

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

История

В символической логике Часть II , Чарльз Доджсон Lutwidge ввел метод деревьев, самое раннее современное использование дерева истины.

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

Смотрите также

Разрешение (логика)

Внешние ссылки

ТАБЛО : ежегодная международная конференция по автоматическому мышлению с аналитическими таблицами и родственными методами.
JAR : Журнал автоматизированных рассуждений
Пакет таблиц : интерактивное средство доказательства логики высказываний и логики первого порядка с использованием таблиц
Генератор доказательства дерева : еще один интерактивный инструмент доказательства логики высказываний и логики первого порядка с использованием таблиц
LoTREC : универсальный инструмент для доказательства модальных логик на основе таблиц от ИРИТ / Тулузского университета

Languages

In other projects