7.4: Таблиця

Last updated
Save as PDF

Page ID: 52674

\( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \) \( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)\(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\) \(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\)

Template:MathJaxZach

Хоча багато систем деривації працюють з домовленостями речень, tableaux працюють зі підписаними формулами. Підписана формула - це пара, що складається зі знака значення істинності (\(\True\)або\(\False\)), а речення\[\sFmla{\True}{A} \text{ or } \sFmla{\False}{A}.\nonumber\] Таблиця складається з підписаних формул, розташованих у дереві, що розгалужується вниз. Вона починається з ряду припущень і продовжується підписаними формулами, які є результатом однієї з підписаних формул над ним шляхом застосування одного з правил умовиводу. Кожне правило дозволяє нам додавати одну або кілька підписаних формул до кінця гілки, або дві підписані формули поруч - у цьому випадку гілка розділяється на дві частини, причому дві додані підписані формули утворюють кінці двох гілок.

Правило, застосоване до складної підписаної формули, призводить до додавання підписаних формул, які є безпосередніми підформулами. Вони приходять парами, по одному правилу для кожного з двох знаків. Наприклад,\(\TRule{\True}{\land}\) правило застосовується і дозволяє\(\sFmla{\True}{A \land B}\) додавати як дві підписані формули, так\(\sFmla{\True}{A}\) і\(\sFmla{\True}{B}\) до кінця будь-якої гілки\(\sFmla{\True}{A \land B}\), що містить, і правило\(\TRule{\False}{A \land B}\) дозволяє гілці бути розділити шляхом додавання\(\sFmla{\False}{A}\) і\(\sFmla{\False}{B}\) пліч-о-пліч. Таблиця закривається, якщо кожна з її гілок містить відповідну пару підписаних формул\(\sFmla{\True}{A}\) і\(\sFmla{\False}{A}\).

\(\Proves\)Відношення, засноване на tableaux, визначається наступним чином:\(\Gamma \Proves A\) якщо є якийсь скінченний набір,\(\Gamma_0 = \{B_1, \dots, B_n\} \subseteq \Gamma\) такий, що існує закрита таблиця\[\{\sFmla{\False}{A}, \sFmla{\True}{B_1}, \dots, \sFmla{\True}{B_n}\}\nonumber\] для припущень Наприклад, ось закрита таблиця, яка показує, що\(\Proves (A \land B) \lif A\) :

\[\begin{array}{lcl} 1. & \False\,(A \land B) \lif A & \text { Assumption } \\ 2 . & \True\, A \land B & \lif \False\, 1 \\ 3 . & \False\, A & \lif \False\, 1 \\ 4 . & \True\, A & \lif \True\, 2 \\ 5 . & \True\, B & \lif \True\, 2 \\ & \otimes & \end{array}\nonumber\]

Набір\(\Gamma\) є неузгодженим у табличному обчисленні, якщо є закрита таблиця для припущень\[\{\sFmla{\True}{B_1}, \dots, \sFmla{\True}{B_n}\}\nonumber\] для деяких\(B_i \in \Gamma\).

Tableaux були винайдені в 1950-х роках самостійно Еверт Бет і Яакко Хінтікка, і спрощені і популяризовані Раймондом Smullyan. Вони дуже прості у використанні, так як побудова столу - дуже систематична процедура. Через систематичність tableaux вони також піддаються реалізації за допомогою комп'ютера. Однак таблицю часто важко читати, і їх зв'язок із доказами іноді нелегко побачити. Підхід також досить загальний, і багато різних логік мають системи таблиць. Tableaux також допомагає нам знайти структури, які задовольняють задані (множини) речень: якщо множина задовольняється, вона не матиме закритої таблиці, тобто будь-яка таблиця матиме відкриту гілку. Задовільна структура може бути «зчитувана» відкритою гілкою, за умови, що кожне правило, яке можна застосувати, було застосовано до цієї гілки. Існує також дуже тісний зв'язок з послідовним численням: по суті, закрита таблиця - це конденсоване похідне в послідовному численні, записане догори дном.