Семантическая таблица

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

Введение

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

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

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

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

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

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

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

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

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

И

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

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

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

• ( ∧ ) A ∧ B A B

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

Или

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

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

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

• ( ∨ ) A ∨ B A | B

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

Не

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

• ( ¬ 1 ) A ¬ ¬ A

• ( ¬ 2 ) ¬ ¬ A A

Закрытие

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

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

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

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

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

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

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

• ( ∧ ) X ∪ { A ∧ B } X ∪ { A , B }

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

• ( ∨ ) X ∪ { A ∨ B } X ∪ { A } | X ∪ { B }

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

• ( i d ) X ∪ { p , ¬ p } c l o s e d

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

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

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

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

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

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

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

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

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

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

Условный

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

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

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

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

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

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

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

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

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

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

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

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