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

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

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

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

История

В своей «Символической логике , часть II» Чарльз Лютвидж Доджсон (также известный под своим литературным псевдонимом Льюис Кэрролл) представил метод деревьев — самое раннее современное использование дерева истинности.

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

Таблицы можно интуитивно рассматривать как последовательные системы перевернутые . Эта симметричная связь между таблицами и секвенциальными системами была формально установлена ​​в (Carnielli 1991).

Пропозициональная логика

Фон

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

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

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

Нотационные варианты связок

соединительный	Символ
И	$A\land B$, $A\cdot B$, $AB$, $A\&B$, $A\&\&B$
эквивалент	$A\equiv B$, $A\Leftrightarrow B$, $A\leftrightharpoons B$
подразумевает	$A\Rightarrow B$, $A\supset B$, $A\rightarrow B$
NAND	$A{\overline {\land }}B$, $A\mid B$, ${\overline {A\cdot B}}$
неэквивалентный	$A\not \equiv B$, $A\not \Leftrightarrow B$, $A\nleftrightarrow B$
НИ	$A{\overline {\lor }}B$, $A\downarrow B$, ${\overline {A+B}}$
НЕТ	$\neg A$, $-A$, ${\overline {A}}$, $\sim A$
ИЛИ	$A\lor B$, $A+B$, $A\mid B$, $A\parallel B$
ИСНО-ИЛИ	$A$ ИСНО-ИЛИ $B$
БЕСПЛАТНО	$A{\underline {\lor }}B$, $A\oplus B$

Общий метод

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

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

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

1. Выберите открытый листовой узел. (Листовой узел в исходной цепочке помечен как открытый).
2. Выберите подходящий узел на ветке над выбранным узлом.
3. Примените соответствующий узел, который соответствует расширению дерева ниже выбранного листового узла на основе некоторого правила расширения (подробно описано ниже).
4. Для каждого вновь созданного узла, который является одновременно литералом/отрицаемым литералом и дополнение которого появляется в предыдущем узле в той же ветви, пометьте ветвь как закрытую . Отметьте все остальные вновь созданные узлы как открытые .

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

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

И

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

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

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

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

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

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

Или

a⋁¬b генерирует a и ¬b

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

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

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

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

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

Нет

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

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

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

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

Закрытие

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

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

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

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

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

Таблица с метками множества

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

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

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

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

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

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

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

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

Ниже представлены две закрытые таблицы набора.

$X=\{r\wedge \neg r,\;p\wedge ((\neg p\vee q)\wedge \neg q)\}$

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

${\dfrac {\quad {\dfrac {\quad r\wedge \neg r,\;p\wedge ((\neg p\vee q)\wedge \neg q)\quad }{r,\;\neg r,\;p\wedge ((\neg p\vee q)\wedge \neg q)}}(\wedge )}{closed}}(\wedge )$

и второй, более длинный, с правилами, применяемыми в другом порядке:

${\dfrac {\quad {\dfrac {\quad {\dfrac {\quad r\wedge \neg r,\;p\wedge ((\neg p\vee q)\wedge \neg q)\quad }{r\wedge \neg r,\;p,\;((\neg p\vee q)\wedge \neg q)}}(\wedge )\quad }{r\wedge \neg r,\;p,\;(\neg p\vee q),\;\neg q}}(\wedge )}{\quad {\dfrac {\quad r\wedge \neg r,\;p,\;\neg p,\;\neg q\quad }{closed}}(id)\quad \quad {\dfrac {\quad r\wedge \neg r,\;p,\;q,\;\neg q\quad }{closed}}(id)}}(\vee )$

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

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

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

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

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

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

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

Условный

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

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

${\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' выполнимо.

Пропозициональная таблица с объединением

Вышеупомянутые правила для пропозициональных таблиц можно упростить, используя единую систему обозначений. В единых обозначениях каждая формула имеет тип $\alpha$ (альфа) или типа $\beta$ (бета). Каждой формуле типа альфа присваиваются два компонента. $\alpha _{1},\alpha _{2}$, и каждой формуле типа бета присваиваются два компонента $\beta _{1},\beta _{2}$. Формулы типа альфа можно рассматривать как конъюнктивные, поскольку обе $\alpha _{1}$ и $\alpha _{2}$ подразумеваются $\alpha$ будучи правдой. Формулы типа бета можно рассматривать как дизъюнктивные, поскольку либо $\beta _{1}$ или $\beta _{2}$ подразумевается под $\beta$ будучи правдой. В таблицах ниже показано, как определить тип и компоненты любой данной пропозициональной формулы:

${\begin{array}{c|c|c}\alpha &\alpha _{1}&\alpha _{2}\\\hline X\wedge Y&X&Y\\\neg (X\vee Y)&\neg X&\neg Y\\\neg (X\implies Y)&X&\neg Y\\\neg \neg X&X&X\\\end{array}}$ ${\begin{array}{c|c|c}\beta &\beta _{1}&\beta _{2}\\\hline \neg (X\wedge Y)&\neg X&\neg Y\\X\vee Y&X&Y\\X\implies Y&\neg X&Y\\\neg \neg X&X&X\\\end{array}}$

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

${\begin{array}{c|c|c}\alpha &\alpha _{1}&\alpha _{2}\\\hline T\,X\wedge Y&T\,\,X&T\,\,Y\\F\,\,X\vee Y&F\,\,X&F\,\,Y\\F\,\,X\implies Y&T\,\,X&F\,\,Y\\F\,\,\neg X&T\,\,X&T\,\,Y\\T\,\,\neg X&F\,\,X&F\,\,Y\end{array}}\qquad {\begin{array}{c|c|c}\beta &\beta _{1}&\beta _{2}\\\hline F\,\,X\wedge Y&F\,\,Y&F\,\,X\\T\,\,X\vee Y&T\,\,X&T\,\,Y\\T\,\,X\implies Y&F\,\,X&T\,\,Y\\F\,\,\neg X&T\,\,X&T\,\,X\\T\,\,\neg X&F\,\,X&F\,\,Y\end{array}}$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

$(\forall ){\frac {\forall x.\gamma (x)}{\gamma (x')}}$ где $x'$ переменная, не встречающаяся нигде в таблице

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

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

$(\sigma )$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Табличное исчисление — это просто набор правил, которые предписывают, как можно изменить таблицу. Процедура доказательства — это метод фактического поиска доказательства (если оно существует). Другими словами, табличное исчисление — это набор правил, а процедура доказательства — это политика применения этих правил. Даже если исчисление является полным, не каждый возможный выбор применения правил приводит к доказательству невыполнимого множества. Например, $\{P(f(c)),R(c),\neg P(f(c))\vee \neg R(c),\forall x.Q(x)\}$ невыполнима, но как таблицы с объединением, так и таблицы без объединения допускают многократное применение правила кванторов всеобщности к последней формуле, тогда как простое применение правила дизъюнкции к третьей непосредственно привело бы к замыканию.

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

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

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

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

Поиск закрытой таблицы

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

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

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

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

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

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

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

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

Пункт таблицы

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

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

$(C){\frac {L_{1}\vee \cdots \vee L_{n}}{L_{1}'|\cdots |L_{n}'}}$ где $L_{1}'\vee \cdots \vee L_{n}'$ получается заменой каждой переменной новой в $L_{1}\vee \cdots \vee L_{n}$

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

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

$(C){\frac {L_{1}\vee \cdots \vee L_{n}}{L_{1}'|\cdots |L_{n}'}}$ где $L_{1}'\vee \cdots \vee L_{n}'$ получается заменой каждой переменной новой в $L_{1}\vee \cdots \vee L_{n}$, который является частью входного набора

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

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

Таблица соединений

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

${\frac {\neg \Box A}{\neg A}}$

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

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

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

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

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

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

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

Всемирно известная картина

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

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

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

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

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

Таблицы маркировки множеств

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Обозначения

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

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

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

Обозначения	Формулы
$\alpha$	$\alpha _{1}\wedge \alpha _{2}$	$\neg ({\overline {\alpha _{1}}}\vee {\overline {\alpha _{2}}})$	$\neg (\alpha _{1}\rightarrow {\overline {\alpha _{2}}})$
$\beta$	$\beta _{1}\vee \beta _{2}$	${\overline {\beta _{1}}}\rightarrow \beta _{2}$	$\neg ({\overline {\beta _{1}}}\wedge {\overline {\beta _{2}}})$
$\gamma$	$\forall x\gamma _{1}(x)$	$\neg \exists x{\overline {\gamma _{1}(x)}}$
$\delta$	$\exists x\delta _{1}(x)$	$\neg \forall x{\overline {\delta _{1}(x)}}$
$\pi$	$\Diamond \pi _{1}$	$\neg \Box {\overline {\pi _{1}}}$
$\nu$	$\Box \nu _{1}$	$\neg \Diamond {\overline {\nu _{1}}}$

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

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

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

Формулы со знаком

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

См. также

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

Ссылки

• Бет, Эверт В. (1955). «Семантическое следствие и формальная выводимость» . Объявления Королевской Нидерландской академии искусств и наук, литературный факультет . 18 (13): 309–42. Перепечатано в Интикка, Джеймс, изд. (1969). Философия математики Издательство Оксфордского университета. ISBN  978-0-19-875011-6 .
• Босток, Дэвид (1997). Промежуточная логика . Издательство Оксфордского университета. ISBN  978-0-19-156707-0 .
• Карниелли, Уолтер А. (1987). «Систематизация конечной многозначной логики методом таблиц» . Журнал символической логики . 52 (2): 473–493. дои : 10.2307/2274395 . JSTOR   2274395 . S2CID   42822367 .
• Карниелли, Уолтер А. (1991). «О секвенциях и таблицах многозначной логики» (PDF) . Журнал неклассической логики . 8 (1): 59–76. Архивировано из оригинала (PDF) 5 марта 2016 г. Проверено 11 октября 2014 г.
• Д'Агостино, М.; Габбай, Д .; Хенле, Р.; Посегга, Дж., ред. (1999). Справочник по табличным методам . Клювер. ISBN  978-94-017-1754-0 .
• Фиттинг, Мелвин (1996) [1990]. Логика первого порядка и автоматическое доказательство теорем (2-е изд.). Нью-Йорк: Спрингер. дои : 10.1007/978-1-4612-2360-3 . ISBN  978-1-4612-7515-2 . S2CID   10411039 .
• Гирле, Род (2014). Модальная логика и философия (2-е изд.). Тейлор и Фрэнсис. ISBN  978-1-317-49217-7 .
• Горе, Раджив. «Табличные методы для модальной и темпоральной логики». Справочник по табличным методам . стр. 297–396.
• Хэнле, Райнер (2001). «3. Таблицы и связанные с ними методы» . В Робинсоне, Алан Дж.А.; Воронков, Андрей (ред.). Справочник по автоматизированному рассуждению . Эльзевир. стр. 101–179. ISBN  978-0-08-053279-0 .
• Хаусон, Колин (11 октября 2005 г.) [1997]. Логика с деревьями: введение в символическую логику . Рутледж. ISBN  978-1-134-78550-6 .
• Джеффри, Ричард (2006) [1967]. Формальная логика: ее объем и пределы (4-е изд.). Хакетт. ISBN  978-0-87220-813-1 .
• Летц, Рейнхольд; Стенц, Гернот. «28. Процедуры исключения модели и таблицы соединений». Справочник по автоматизированному рассуждению . стр. 2015–2114 гг.
• Смалльян, Раймонд (1995) [1968]. Логика первого порядка . Дувр. ISBN  978-0-486-68370-6 .
• Смуллян, Раймонд (2014). Руководство для начинающих по математической логике . Дувр. ISBN  978-0486492377 .
• Энциклопедия философии, изд. (11 декабря 2023 г.). «Современная логика: булев период: Кэрролл» . Энциклопедия философии . Проверено 26 декабря 2023 г.
• Земан, Джозеф Джей (1973). Модальная логика: модальные системы Льюиса . Кларендон Пресс. ISBN  978-0-19-824374-8 . OCLC   641504 .

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

• TABLEAUX : ежегодная международная конференция по автоматизированному рассуждению с помощью аналитических таблиц и связанных с ними методов.
• JAR : Журнал автоматизированных рассуждений
• Пакет tableaux : интерактивное средство доказательства пропозициональной логики и логики первого порядка с использованием таблиц.
• Генератор доказательства дерева : еще одно интерактивное средство доказательства для логики высказываний и логики первого порядка с использованием таблиц.
• LoTREC : универсальное средство доказательства модальной логики на основе таблиц от IRIT/Тулузского университета.
• Знакомство с деревьями истины на YouTube