Метод аналитических таблиц

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

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

Введение [ править ]

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

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

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

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

Логика высказываний [ править ]

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

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

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

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

И [ править ]

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

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

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

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

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

Или [ редактировать ]

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

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

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

${\displaystyle (\vee ){\frac {A\vee B}{A\mid B}}}$

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

Не [ редактировать ]

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

${\displaystyle (\neg 1){\frac {A}{\neg \neg A}}}$

${\displaystyle (\neg 2){\frac {\neg \neg A}{A}}}$

Закрытие [ править ]

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

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

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

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

Таблица с метками [ править ]

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

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

${\displaystyle (\wedge ){\frac {X\cup \{A\wedge B\}}{X\cup \{A,B\}}}}$

Для дизъюнкции набор эквивалентен дизъюнкции двух множеств и . В результате, если первый набор помечает лист, к нему могут быть добавлены два дочерних элемента, помеченные двумя последними формулами.${\displaystyle X\cup \{A\vee B\}}$${\displaystyle X\cup \{A\}}$${\displaystyle X\cup \{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 \wedge }$${\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)} -------------------------------------(я бы) ---------- ------------------------------------------------ (& ) замкнутые {r0 & ~ r0, p0, (~ p0 v q0), ~ q0}  -------------------------------------------------- ----------- (v) {r0 & ~ r0, p0, ~ p0, ~ q0} | {r0 & ~ r0, p0, q0, ~ q0} -------------------------- (я бы) --------------------- - (я бы) закрыто закрыто

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

Три правил , и приведенные выше, то достаточно , чтобы решить , является ли данный набор формул в отрицаются нормальной форма совместно выполним:${\displaystyle (\wedge )}$${\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\Leftrightarrow B&=&(A\land B)\lor (\neg A\land \neg B)\\\neg (A\Leftrightarrow B)&=&(A\land \neg B)\lor (\neg A\land B)\end{array}}}$

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

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

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

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

Таблица первого порядка без объединения [ править ]

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

${\displaystyle (\forall ){\frac {\forall x.\gamma (x)}{\gamma (t)}}}$где - произвольный основной член${\displaystyle t}$

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

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

${\displaystyle (\exists ){\frac {\exists x.\delta (x)}{\delta (c)}}}$где новый постоянный символ${\displaystyle c}$

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

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

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

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

Таблица первого порядка с объединением [ править ]

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

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

${\displaystyle (\forall ){\frac {\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(a),\forall x.P(x)\}}$${\displaystyle P(x_{1})}$${\displaystyle \neg P(a)}$${\displaystyle x_{1}}$${\displaystyle a}$${\displaystyle P(x_{1})}$${\displaystyle P(a)}$

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

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

${\displaystyle (\exists ){\frac {\exists x.\delta (x)}{\delta (f(x_{1},\ldots ,x_{n}))}}}$где - символ новой функции, а свободные переменные${\displaystyle f}$${\displaystyle x_{1},\ldots ,x_{n}}$${\displaystyle \delta }$

Это правило включает упрощение по сравнению с правилом, в котором являются свободными переменными ветви, а не только. Это правило можно дополнительно упростить путем повторного использования символа функции, если он уже использовался в формуле, идентичной переименованию переменной.${\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 \gamma (x')}$${\displaystyle \gamma }$${\displaystyle x'}$${\displaystyle \gamma (t)}$${\displaystyle t}$${\displaystyle x}$
• Свободные переменные в таблице жесткие: все вхождения одной и той же переменной должны быть заменены одним и тем же термином. Каждую переменную можно рассматривать как символ, представляющий термин, который еще не определен. Это является следствием того, что свободные переменные считаются универсально количественно оцененными по всей формуле, представленной таблицей: если одна и та же переменная встречается бесплатно в двух разных узлах, оба вхождения находятся в области действия одного и того же квантификатора. Например, если формулы в двух узлах и , где свободны в обоих, формула, представленная таблицей, является чем-то в форме . Эта формула подразумевает, что это верно для любого значения , но в целом не подразумевает для двух разных членов и${\displaystyle A(x)}$${\displaystyle B(x)}$${\displaystyle x}$${\displaystyle \forall x.(...A(x)...B(x)...)}$${\displaystyle (...A(x)...B(x)...)}$${\displaystyle x}$${\displaystyle (...A(t)...A(t')...)}$${\displaystyle t}$${\displaystyle t'}$, поскольку эти два члена могут принимать разные значения. Это означает, что нельзя заменить двумя разными терминами в и .${\displaystyle x}$${\displaystyle A(x)}$${\displaystyle B(x)}$
• Свободные переменные в формуле для проверки действительности также считаются универсально определенными. Однако эти переменные нельзя оставлять свободными при построении таблицы, потому что правила таблицы работают с обратной формулой, но по-прежнему рассматривают свободные переменные как универсально количественно определяемые. Например, неверно (неверно в модели 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 \{P(f(c)),R(c),\neg P(f(c))\vee \neg R(c),\forall x.Q(x)\}}$

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

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

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

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

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

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

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

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

Сокращение поиска [ править ]

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

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

Различные методы сокращения поиска запрещают создание некоторых таблиц на том основании, что замкнутая таблица все еще может быть найдена путем расширения других. Эти ограничения называются глобальными. В качестве примера глобального ограничения можно использовать правило, определяющее, какая из открытых ветвей должна быть расширена. В результате, если таблица имеет, например, две незамкнутые ветви, правило указывает, какая из них должна быть расширена, запрещая расширение второй. Это ограничение сокращает пространство поиска, потому что один возможный выбор теперь запрещен; полнота, однако, не пострадает, так как вторая ветвь все равно будет расширена, если первая в конечном итоге будет закрыта. В качестве примера, таблицы с корневыми , ребенок , и два листа и могут быть закрыты двумя способами: нанесение${\displaystyle \neg a\wedge \neg b}$${\displaystyle a\vee b}$${\displaystyle a}$${\displaystyle b}$${\displaystyle (\wedge )}$сначала к, а затем к , или наоборот. Очевидно, нет необходимости использовать обе возможности; можно рассматривать только тот случай, когда он применяется впервые, и игнорировать случай, в котором он применяется впервые . Это глобальное ограничение, потому что этим вторым расширением можно пренебречь наличие другой таблицы, где расширение применяется к первой и последующим.${\displaystyle a}$${\displaystyle b}$${\displaystyle (\wedge )}$${\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 P(x,y)\vee Q(f(x))}$${\displaystyle \forall x,y.P(x,y)\vee Q(f(x))}$${\displaystyle P(x,y)\vee Q(f(x))}$${\displaystyle \exists x,y.P(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_{n}}$

Когда набор, который нужно проверить на выполнимость, состоит только из пунктов, этого и правил унификации достаточно, чтобы доказать невыполнимость. В других мирах, в Tableau исчисления состоят из и являются полным.${\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_{n}}$

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

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

Таблица соединений [ править ]

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

сильная связанность

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

слабая связанность

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

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

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

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

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

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

Обычные картины [ править ]

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

Однако эти запрещенные шаги расширения бесполезны. Если это ветвь, содержащая литерал , и предложение, расширение которого нарушает регулярность, тогда содержит . Чтобы закрыть таблицу, нужно, в том числе, развернуть и закрыть ветвь, где , где встречается дважды. Однако формулы в этой ветке точно такие же, как и формулы одной. В результате те же шаги расширения, которые закрываются, также закрываются . Это означает, что в расширении не было необходимости; кроме того, если${\displaystyle B}$${\displaystyle L}$${\displaystyle C}$${\displaystyle C}$${\displaystyle L}$${\displaystyle B-L}$${\displaystyle L}$${\displaystyle B}$${\displaystyle B-L}$${\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 a\wedge \neg \Box a}$${\displaystyle a}$${\displaystyle a}$${\displaystyle (\wedge )}$${\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\wedge \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\wedge \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\wedge 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)}$

Set-labeling tableaux [ править ]

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

Таблицы модальных логик используются для проверки выполнимости набора модальных формул в данной модальной логике. По заданному набору формул они проверяют существование такой модели и мира , что .${\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 (\theta )}$

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

Аксиома 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 (a\wedge \neg \Box a)}$${\displaystyle (T),(\wedge ),(\theta ),(K)}$${\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\wedge 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 \alpha _{1}\wedge \alpha _{2}}$

Обозначение	Формулы
${\displaystyle \alpha }$	${\displaystyle \alpha _{1}\wedge \alpha _{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}}}\wedge {\overline {\beta _{2}}})}$
${\displaystyle \gamma }$	${\displaystyle \forall x\gamma _{1}(x)}$	${\displaystyle \neg \exists x{\overline {\gamma _{1}(x)}}}$
${\displaystyle \delta }$	${\displaystyle \exists x\delta _{1}(x)}$	${\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 (a\vee b)}$${\displaystyle \alpha _{1}}$${\displaystyle a}$

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

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

Подписанные формулы [ править ]

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

История [ править ]

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

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

См. Также [ править ]

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

Ссылки [ править ]

• Бет, Эверт В., 1955. «Семантическое следование и формальная выводимость», Mededelingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde , NR Vol 18, No. 13, 1955, pp 309–42. Перепечатано в Jaakko Intikka (ed.) The Philosophy of Mathematics , Oxford University Press, 1969.
• Босток, Дэвид, 1997. Промежуточная логика . Oxford Univ. Нажмите.
• М. Д'Агостино, Д. Габбей, Р. Хенле, Дж. Посегга (редакторы), Справочник по табличным методам , Kluwer, 1999.
• Гирле, Род, 2000. Модальная логика и философия . Теддингтон Великобритания: Проницательность.
• Горе, Раджив (1999) «Табличные методы для модальной и временной логики» в Д'Агостино, М., Дов Габбай, Р. Хенле и Дж. Посегга, ред., Справочник по табличным методам . Kluwer: 297-396.
• Ричард Джеффри , 1990 (1967). Формальная логика: ее объем и пределы , 3-е изд. Макгроу Хилл.
• Раймонд Смуллян , 1995 (1968). Логика первого порядка . Dover Publications.
• Мелвин Фиттинг (1996). Логика первого порядка и автоматическое доказательство теорем (2-е изд.). Springer-Verlag.
• Райнер Хенле (2001). Таблицы и родственные методы. Справочник по автоматическому мышлению
• Райнхольд Летц, Гернот Стенц (2001). Процедуры исключения модели и таблицы соединений. Справочник по автоматическому мышлению
• Земан, Дж. Дж. (1973) Модальная логика. Рейдел.

Внешние ссылки [ править ]

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