分析表法

無限集合を仮定する${\displaystyle PV}$命題変数の集合を定義し、${\displaystyle \Phi }$帰納法による論理式の導出は、以下の文法で表される。

${\displaystyle \Phi$ ::=PV\mid \neg \Phi \mid (\Phi \to \Phi )\mid (\Phi \lor \Phi )\mid (\Phi \land \Phi )} 。

つまり、基本的な接続詞は否定です。${\displaystyle \neg }$意味​${\displaystyle \to }$選言​${\displaystyle \lor }$、および接続詞${\displaystyle \land }$。

式の真偽は、その式の真理値と呼ばれます。式、または式の集合は、命題変数に真理値を割り当てることで、変数と結合子を組み合わせた式全体が真になるような割り当てが可能である場合に、充足可能であると言われます。 ^{[ 1 ]}このような割り当ては、式を満たすと言われます。 ^{[ 2 ]}

タブローは、与えられた一連の式が充足可能かどうかをチェックします。これは、妥当性または含意のどちらかをチェックするために使用できます。式は、その否定が充足不可能である場合に有効であり、式は${\displaystyle A_{1},\ldots ,A_{n}}$暗示する${\displaystyle B}$もし${\displaystyle \{A_{1},\ldots ,A_{n},\neg B\}}$満たされない。

任意の数式について${\displaystyle X}$、${\displaystyle Y}$以下の事実が成り立つ。

• 接続詞​${\displaystyle X\land Y}$    そうだとすれば${\displaystyle X}$、${\displaystyle Y}$両方とも真である。が偽である場合、    ${\displaystyle X}$偽または${\displaystyle Y}$誤りです。
• 論理和が${\displaystyle X\lor Y}$    が真であれば、${\displaystyle X}$真または${\displaystyle Y}$が真であるならば、が偽であるならば、    ${\displaystyle X}$、${\displaystyle Y}$どちらも誤りです。
• 条件付きの場合${\displaystyle X\to Y}$    が真であれば、${\displaystyle X}$偽または${\displaystyle Y}$が真であるならば、が偽であるならば、    ${\displaystyle X}$真実であり、${\displaystyle Y}$誤りです。
• 否定の場合${\displaystyle \neg X}$    そうだとすれば${\displaystyle X}$偽である。偽であるならば、    ${\displaystyle X}$それは本当です。

分析タブロー法は、これらの事実に基づいている。命題タブロー法の主な原理は、相補的なリテラルのペアが生成されるか、それ以上の展開が不可能になるまで、複雑な式をより小さな式に「分解」しようとすることである。

この方法は、ノードに数式がラベル付けされた木構造に対して機能します。各ステップでこの木構造が変更されます。命題論理の場合、許可される変更は葉ノードの子孫としてノードを追加することのみです。手順は、充足不能性を証明するために、集合内のすべての数式の連鎖からなる木構造を生成することから始まります。^{[ 11 ]}次に、以下の手順を非決定的に繰り返し適用することができます。

1. 開いている葉ノードを選択してください。（初期チェーンの葉ノードは「開いている」とマークされています。）
2. 選択したノードの上のブランチで、該当するノードを選択してください。^{[ 12 ]}
3. 該当するノードを適用します。これは、選択したリーフノードの下のツリーを、何らかの展開ルール（詳細は後述）に基づいて展開することに対応します。
4. 新しく作成されたノードがリテラルまたは否定リテラルであり、かつその補数が同じブランチ上の前のノードに存在する場合、そのブランチを閉じた状態としてマークします。その他の新しく作成されたノードはすべて開いた状態としてマークします。

タブローのブランチに数式が含まれている場合...

• $\displaystyle {\boldsymbol {\mathsf {T}}}(X\land Y)}$、その葉に、式を含む2つのノードの連鎖を追加する${\displaystyle {\boldsymbol {\mathsf {T}}}(X)}$そして${\displaystyle {\boldsymbol {\mathsf {T}}}(Y)}$; ^{[ 13 ]}
• $\displaystyle {\boldsymbol {\mathsf {F}}}(X\land Y)}$、その葉に2つの兄弟子を作成し、式を含める$\displaystyle {\boldsymbol {\mathsf {F}}}(X)}$そして${\displaystyle {\boldsymbol {\mathsf {F}}}(Y)}$それぞれ; ^{[ 14 ]}
• $\displaystyle {\boldsymbol {\mathsf {T}}}(X\lor Y)}$、その葉に2つの兄弟子を作成し、式を含める${\displaystyle {\boldsymbol {\mathsf {T}}}(X)}$そして${\displaystyle {\boldsymbol {\mathsf {T}}}(Y)}$それぞれ;
• $\displaystyle {\boldsymbol {\mathsf {F}}}(X\lor Y)}$、その葉に、式を含む2つのノードの連鎖を追加する$\displaystyle {\boldsymbol {\mathsf {F}}}(X)}$そして${\displaystyle {\boldsymbol {\mathsf {F}}}(Y)}$;
• $\displaystyle {\boldsymbol {\mathsf {T}}}(X\to Y)}$、その葉に2つの兄弟子を作成し、式を含める$\displaystyle {\boldsymbol {\mathsf {F}}}(X)}$そして${\displaystyle {\boldsymbol {\mathsf {T}}}(Y)}$それぞれ;
• ${\displaystyle {\boldsymbol {\mathsf {F}}}(X\to Y)}$、その葉に、式を含む2つのノードの連鎖を追加する${\displaystyle {\boldsymbol {\mathsf {T}}}(X)}$そして${\displaystyle {\boldsymbol {\mathsf {F}}}(Y)}$;
• $\displaystyle {\boldsymbol {\mathsf {T}}}(\neg X)}$、その葉に式を含むノードを追加する$\displaystyle {\boldsymbol {\mathsf {F}}}(X)}$;
• $\displaystyle {\boldsymbol {\mathsf {F}}}(\neg X)}$、その葉に式を含むノードを追加する${\displaystyle {\boldsymbol {\mathsf {T}}}(X)}$。

分解プロセスは有限のステップ数で終了します。なぜなら、規則を適用するたびに結合子が1つ削除され、どの式にも結合子は有限個しか存在しないからです。

注：文法に基づくシステムでは

${\displaystyle \Phi$ ::=\bot \mid PV\mid (\Phi \to \Phi )\mid (\Phi \lor \Phi )\mid (\Phi \land \Phi )} 、

否定を原始的なものとして扱わず、含意と偽りの観点から定義する（${\displaystyle \neg \Phi \,{\overset {\text{def}}{=}}\,\Phi \to \bot }$)タブロールール${\displaystyle \neg }$に置き換えられる

タブローの原理は、同じブランチのノードにある式は連言として扱われ、異なるブランチの式は選言として扱われるというものです。結果として、タブローは連言の選言である式のツリー状の表現となります。この式は、充足不能性を証明するための集合と同等です。この手順では、結果として得られるタブローによって表される式が元の式と同等になるようにタブローを変更します。これらの連言のいずれかに相補的なリテラルのペアが含まれる場合、その連言は充足不能であることが証明されます。すべての連言が充足不能であることが証明された場合、元の式の集合は充足不能となります。

すべてのタブローは、タブローが構築された集合と等価な式のグラフィカル表現とみなすことができます。この式は次のとおりです。タブローの各枝は、その式同士の論理積を表し、タブロー自体は、その枝同士の論理和を表します。展開規則は、タブローを、等価な式を表すタブローに変換します。タブローは入力集合の式を含む単一の枝として初期化されるため、そこから得られる後続のすべてのタブローは、その集合と等価な式を表します（初期タブローが「true」とラベル付けされた単一のノードであるバリアントでは、タブローによって表される式は、元の集合の結果です）。

タブロー法は、まず一連の式から始め、タブローにさらに単純な式を追加していき、反対のリテラルの単純な形で矛盾が示されるまで続けることで機能します。タブローで表される式は、その枝で表される式の選言であるため、すべての枝に反対のリテラルのペアが含まれる場合に矛盾が生じます。

分岐にリテラルとその否定が含まれると、対応する式は充足不可能になります。その結果、この分岐はこれ以上展開する必要がないため、「閉じる」ことができます。タブローのすべての分岐が閉じている場合、タブローで表される式は充足不可能になります。したがって、元の集合も充足不可能になります。すべての分岐が閉じているタブローを得ることは、元の集合の充足不可能性を証明する方法の一つです。命題論理の場合、すべての展開規則が適用可能なすべての場所に適用されている限り、閉じたタブローを見つけることが不可能であることから充足可能性が証明されることも証明できます。特に、タブローにいくつかの開いた（閉じていない）分岐があり、リテラルではないすべての式が、その式が含まれるすべての分岐で新しいノードを生成する規則によって使用されている場合、その集合は充足可能です。

この規則は、式が複数の分岐に存在する可能性があることを考慮に入れています（これは、ノードの「下」に少なくとも1つの分岐点が存在する場合に該当します）。この場合、式を展開するための規則を適用して、まだ開いているすべての分岐にその結論を追加する必要があります。そうして初めて、タブローをこれ以上展開できないこと、したがって式が充足可能であることを結論付けることができます。

命題タブローに関する上記の規則は、統一表記法を用いることで簡略化できる。統一表記法では、各式は次のいずれかのタイプとなる。${\displaystyle \alpha }$（アルファ）またはタイプ${\displaystyle \beta }$（ベータ）。アルファ型の各式には、2つのコンポーネントが割り当てられます。$\alpha_1, \alpha_2$、そしてベータ型の各式には2つの成分が割り当てられる。${\displaystyle \beta _{1},\beta _{2}}$アルファ型の式は連言的であると考えることができる。$\displaystyle \alpha _{1}}$そして$\displaystyle \alpha _{2}}$暗示されている${\displaystyle \alpha }$真であること。ベータ型の式は、選言的であると考えることができる。$\displaystyle \beta _{1}}$または$\displaystyle \beta _{2}}$は、${\displaystyle \beta }$真であること。以下の表は、任意の命題論理式の型と構成要素を決定する方法を示しています。^{[ 15 ]}

各表において、左端の列はアルファ型またはベータ型の式について考えられるすべての構造を示し、右端の列はそれぞれの構成要素を示しています。

上記の表記法を用いて命題タブローを構築する際、アルファ型の式に遭遇するたびに、その2つの構成要素は${\displaystyle \alpha _{1},\alpha _{2}}$展開中の現在のブランチに追加されます。${\displaystyle \theta }$分割できる${\displaystyle \theta }$2 つのブランチに分割され、1 つはセット {${\displaystyle \theta }$、${\displaystyle \beta _{1}}$} の数式、そしてもう 1 つの数式は {${\displaystyle \theta }$、${\displaystyle \beta _{2}}$} の数式。^{[ 16 ]}

タブローの変形として、単一の式ではなく式の集合でノードにラベルを付ける方法がある。^{[ 17 ]}この場合、最初のタブローは、充足可能であることを証明する集合でラベル付けされた単一のノードである。したがって、集合内の式は連言されているとみなされる。

タブローの拡張ルールは、タブローの葉ノードに対して適用され、内部ノードはすべて無視されます。論理積の場合、ルールは論理積を含む集合の同値性に基づいています。${\displaystyle A\land B}$両方を含むセット${\displaystyle A}$そして${\displaystyle B}$その代わりに。特に、葉にラベルが付けられている場合は、${\displaystyle X\cup \{A\land B\}}$ノードにラベルを追加できます${\displaystyle X\cup \{A,B\}}$:

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

論理和の場合、集合${\displaystyle X\cup \{A\lor B\}}$これは2つの集合の論理和に相当する。${\displaystyle X\cup \{A\}}$そして${\displaystyle X\cup \{B\}}$その結果、最初のセットが葉にラベルを付けている場合、2つの子要素をその葉に追加することができ、それらの子要素には後の2つの式でラベルを付けることができます。

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

最後に、ある集合にリテラルとその否定の両方が含まれている場合、この分岐は閉じることができます。

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

与えられた有限集合Xに対するタブローとは、根がXである有限（逆さま）ツリーであり、そのすべての子ノードは、タブロー規則を親ノードに適用することによって得られる。このようなタブローの枝は、葉ノードに「closed」が含まれている場合に閉じている。タブローは、すべての枝が閉じている場合に閉じている。タブローは、少なくとも 1 つの枝が閉じていない場合に開いている。

以下は、セットの閉じた2つのタブローです。

${\displaystyle X=\{r\land \neg r,\;p\land ((\neg p\lor q)\land \neg q)\}}$

各ルールの適用箇所は右側に示されています。どちらも同じ効果が得られますが、最初のルールの方が処理が早く完了します。唯一の違いは、削減処理の順序です。

${\displaystyle {\dfrac {\quad {\dfrac {\quad r\land \neg r,\;p\land ((\neg p\lor q)\land \neg q)\quad }{r,\;\neg r,\;p\land ((\neg p\lor q)\land \neg q)}}(\land )}{closed}}(\land )}$

そして2つ目は、より長いもので、ルールが異なる順序で適用される。

${\displaystyle {\dfrac {\quad {\dfrac {\quad {\dfrac {\quad r\land \neg r,\;p\land ((\neg p\lor q)\land \neg q)\quad }{r\land \neg r,\;p,\;((\neg p\lor q)\land \neg q)}}(\land )\quad }{r\land \neg r,\;p,\;(\neg p\lor q),\;\neg q}}(\land )}{\quad {\dfrac {\quad r\land \neg r,\;p,\;\neg p,\;\neg q\quad }{closed}}(id)\quad \quad {\dfrac {\quad r\land \neg r,\;p,\;q,\;\neg q\quad }{closed}}(id)}}(\lor )}$

最初のタブローはルールを1回適用するだけで閉じますが、2番目のタブローはうまくいかず、閉じるのにずっと時間がかかります。当然ながら、常に最短の閉じたタブローを見つけるのが望ましいのですが、すべての入力式セットに対して最短の閉じたタブローを見つける単一のアルゴリズムは存在しないことが示されています。

３つのルール${\displaystyle (\land )}$、${\displaystyle (\lor )}$そして${\displaystyle (id)}$上記のものは、与えられたセットが${\displaystyle X'}$否定正規形の式のうち、共同で充足可能なものは以下のとおりです。

すべての可能なルールをすべての可能な順序で適用して、閉じたタブローを見つけます。${\displaystyle X'}$または、あらゆる可能性を尽くして、すべてのタブローが${\displaystyle X'}$営業中です。

最初のケースでは、${\displaystyle X'}$は共同で充足不可能であり、2番目のケースでは、開いた枝の葉ノードが原子式と否定された原子式に割り当てを与え、${\displaystyle X'}$共同で充足可能。古典論理には、実際には、(任意の) 1 つのタブローを完全に調査するだけでよいという非常に良い性質があります。もしそれが閉じているならば、${\displaystyle X'}$満たされない、そしてもしそれが開いているならば${\displaystyle X'}$充足可能である。しかし、この性質は一般的に他の論理体系には見られない。

これらの規則は、初期論理式集合Xを取り、各要素C を論理的に等価な否定正規形C'に置き換えることで論理式集合X'を得ることにより、古典論理のすべてに対応できます。X が充足可能であるのは、X' が充足可能である場合のみであることがわかっ ているので、上記の手順を使用してX'の閉タブローを探索すれば十分です。

設定することで${\displaystyle X=\{\neg A\}}$式Aが古典論理のトートロジーであるかどうかをテストすることができる。

もしタブローが${\displaystyle \{\neg A\}}$閉じてから${\displaystyle \neg A}$は充足不可能であり、したがってAはトートロジーである。なぜなら、真理値の割り当てによってA が偽になることは決してないからである。そうでなければ、任意の開いたタブローの任意の開いた枝の任意の開いた葉は、${\displaystyle \{\neg A\}}$Aを偽る課題を与える。

一次式${\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)\lor \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}$新しい定数記号です

スコレム用語${\displaystyle c}$は定数（アリティ0 の関数）です。なぜなら、 上の量化は${\displaystyle x}$はどの全称量化子の範囲内にも発生しません。元の式に全称量化子が含まれていて、その量化が${\displaystyle x}$これらの数量詞は、その範囲内であったため、全称数量詞の規則を適用することにより明らかに削除されました。

存在量化子の規則では新しい定数記号が導入されます。これらの記号は全称量化子の規則で使用できるため、${\displaystyle \forall y.\gamma (y)}$生成できる${\displaystyle \gamma (c)}$たとえ${\displaystyle c}$これは元の式には含まれていませんでしたが、存在量化子の規則によって作成されたスコレム定数です。

全称量化子と存在量化子に関する上記の2つの規則は正しく、命題規則も同様です。つまり、ある論理式の集合が閉じたタブローを生成する場合、その集合は充足不可能です。完全性も証明できます。ある論理式の集合が充足不可能であれば、これらの規則によってそこから構築された閉じたタブローが存在します。ただし、実際にそのような閉じたタブローを見つけるには、規則の適用に関する適切な方針が必要です。そうでない場合、充足不可能な集合は無限に拡大するタブローを生成する可能性があります。例として、集合 が挙げられます。${\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}$全称量化子規則の場合。実際、考えられるすべての基本項を使用できますが、明らかにそれらのほとんどはタブローを閉じるのに役立たない可能性があります。

この問題の解決策は、規則の帰結がタブローの少なくとも1つの分岐を閉じることを可能にする時点まで項の選択を「遅らせる」ことです。これは、項の代わりに変数を使用することで実現できます。${\displaystyle \forall x.\gamma (x)}$生成する${\displaystyle \gamma (x')}$そして、後から置換を許可する${\displaystyle x'}$項を加えると、全称量化子の規則は次のようになります。

${\displaystyle (\forall ){\frac {\forall x.\gamma (x)}{\gamma (x')}}}$どこ${\displaystyle x'}$これは、表の他のすべての場所には出現しない変数です。

当初の数式セットには自由変数が含まれていないことが前提とされているが、この表の数式には、この規則によって生成された自由変数が含まれる可能性がある。これらの自由変数は、暗黙のうちに全称量化されているとみなされる。

このルールでは、基本項の代わりに変数を使用します。この変更によって得られる利点は、タブローの分岐が閉じられるときにこれらの変数に値を割り当てることができるため、役に立たない可能性のある項が生成されるという問題を解決できることです。

例えば、${\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)}$これでこの場面は終わりを迎える。

この規則は、少なくともタブローの1つの分岐（対象となるリテラルのペアを含む分岐）を閉じます。ただし、置換はこれら2つのリテラルだけでなく、タブロー全体に適用する必要があります。これは、タブローの自由変数が固定されている、つまり、ある変数の出現箇所が別のものに置き換えられた場合、同じ変数の他のすべての出現箇所も同様に置き換えられなければならない、という形で表現されます。形式的には、自由変数は（暗黙的に）全称量化されており、タブローのすべての式はこれらの量化子の範囲内にあります。

存在量化子はスコレム化によって処理されます。統一のないタブローとは異なり、スコレム項は単純な定数であってはなりません。実際、統一のあるタブローの式には自由変数が含まれることがあり、それらは暗黙のうちに全称量化されているとみなされます。その結果、次のような式は${\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}$と。
• タブロー内の自由変数は固定されています。つまり、同じ変数のすべての出現箇所は、すべて同じ項に置き換えられなければなりません。すべての変数は、まだ決定されていない項を表す記号とみなすことができます。これは、自由変数がタブローによって表される式全体にわたって普遍的に量化されていると仮定されていることの結果です。同じ変数が2つの異なるノードで自由に出現する場合、両方の出現箇所は同じ量化子の範囲内にあります。例として、2つのノードの式が次のようになっている場合、${\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')...)}$2つの異なる期間${\displaystyle t}$そして${\displaystyle t'}$なぜなら、これら2つの項は一般的に異なる値をとる可能性があるからです。これはつまり、${\displaystyle x}$2つの異なる用語で置き換えることはできません${\displaystyle A(x)}$そして${\displaystyle B(x)}$。
• Free variables in a formula to check for validity are also considered universally quantified. However, these variables cannot be left free when building a tableau, because tableau rules works on the converse of the formula but still treats free variables as universally quantified. For example, ${\displaystyle P(x)\to P(c)}$ is not valid (it is not true in the model where ${\displaystyle D=\{1,2\},P(1)=\bot ,P(2)=\top ,c=1}$, and the interpretation where ${\displaystyle x=2}$). Consequently, ${\displaystyle \{P(x),\neg P(c)\}}$ is satisfiable (it is satisfied by the same model and interpretation). However, a closed tableau could be generated with ${\displaystyle P(x)}$ and ${\displaystyle \neg P(c)}$, and substituting ${\displaystyle x}$ with ${\displaystyle c}$ would generate a closure. A correct procedure is to first make universal quantifiers explicit, thus generating ${\displaystyle \forall x.(P(x)\to P(c))}$.

The following two variants are also correct.

• Applying to the whole tableau a substitution to the free variables of the tableau is a correct rule, provided that this substitution is free for the formula representing the tableau. In other worlds, applying such a substitution leads to a tableau whose formula is still a consequence of the input set. Using most general unifiers automatically ensures that the condition of freeness for the tableau is met.
• While in general every variable has to be replaced with the same term in the whole tableau, there are some special cases in which this is not necessary.

Tableaux with unification can be proved complete: if a set of formulae is unsatisfiable, it has a tableau-with-unification proof. However, actually finding such a proof may be a difficult problem. Contrarily to the case without unification, applying a substitution can modify the existing part of a tableau; while applying a substitution closes at least a branch, it may make other branches impossible to close (even if the set is unsatisfiable).

A solution to this problem is delayed instantiation: no substitution is applied until one that closes all branches at the same time is found. With this variant, a proof for an unsatisfiable set can always be found by a suitable policy of application of the other rules. This method however requires the whole tableau to be kept in memory: the general method closes branches, which can be then discarded, while this variant does not close any branch until the end.

The problem that some tableaux that can be generated are impossible to close even if the set is unsatisfiable is common to other sets of tableau expansion rules: even if some specific sequences of application of these rules allow constructing a closed tableau (if the set is unsatisfiable), some other sequences lead to tableaux that cannot be closed. General solutions for these cases are outlined in the "Searching for a tableau" section.

探索木のサイズは、与えられた（親）タブローから生成できる（子）タブローの数に依存します。したがって、そのようなタブローの数を減らすことで、必要な探索を減らすことができます。

この数を減らす方法の一つは、内部構造に基づいて一部のタブローの生成を禁止することです。例えば、規則性の条件が挙げられます。ある分岐にリテラルが含まれている場合、同じリテラルを生成する展開規則を使用しても意味がありません。なぜなら、リテラルのコピーが2つ含まれる分岐は、元の分岐と同じ数式セットを持つことになるからです。閉じたタブローが存在する場合、この展開なしでもタブローを見つけることができるため、この展開を禁止することができます。この制限は構造的なものであり、タブローの構造を調べて展開のみを行うことでチェックできます。

探索範囲を縮小するさまざまな方法では、閉じたタブローが他のタブローを展開することで見つかる可能性があるという理由で、一部のタブローの生成を禁止します。これらの制限はグローバル制限と呼ばれます。グローバル制限の例として、開いているブランチのうちどれを展開するかを指定するルールを用いることができます。結果として、タブローに例えば2つの閉じていないブランチがある場合、ルールはどちらを展開するかを指定し、2番目のブランチの展開を禁止します。この制限により、可能な選択肢の1つが禁止されるため、探索空間が縮小されます。ただし、最初のブランチが最終的に閉じられた場合、2番目のブランチは展開されるため、完全性は損なわれません。例として、ルートを持つタブローを考えてみましょう。${\displaystyle \neg a\land \neg b}$、 子供${\displaystyle a\lor b}$、そして2枚の葉${\displaystyle a}$そして${\displaystyle b}$2つの方法で閉じることができます:適用する${\displaystyle (\land )}$最初に${\displaystyle a}$そして${\displaystyle b}$、あるいはその逆。両方の可能性を追う必要は明らかにありません。次のケースのみを考慮すればよいでしょう。${\displaystyle (\land )}$最初に適用されるのは${\displaystyle a}$そして、それが最初に適用されるケースを無視する${\displaystyle b}$これはグローバルな制約です。なぜなら、この2番目の展開を無視できるのは、展開が適用されるもう1つのタブローの存在によるからです。${\displaystyle a}$最初に${\displaystyle b}$その後。

接続とは、タブロー上の条件であり、既にブランチ内に存在するリテラルとは無関係な節を使用してブランチを展開することを禁止するものです。接続は、次の2つの方法で定義できます。

強い繋がり

ブランチを展開する際、入力句が現在のリーフ内のリテラルの否定と統一可能なリテラルを含む場合にのみ、入力句を使用する。

弱い連結性

分岐上のリテラルの否定と統一するリテラルを含む節の使用を許可する

どちらの条件も、ルートだけでなく他の要素も含むブランチにのみ適用されます。2番目の定義では、ブランチ内のリテラルの否定と統一するリテラルを含む節の使用が認められますが、1番目の定義では、そのリテラルが現在のブランチのリーフにあるという制約がさらに追加されます。

節の拡張が連結性（強連結または弱連結）によって制限されている場合、その適用により、新しい葉のいずれかに置換を適用してその枝を閉じることができるタブローが生成されます。具体的には、これは、枝内のリテラルの否定と統一する節のリテラルを含む葉（または、強連結の場合は親のリテラルの否定を含む葉）です。

連結性のどちらの条件も、完全な一階述語論理につながります。節の集合が充足不能である場合、それは閉じた連結（強連結または弱連結）タブローを持ちます。このような閉じたタブローは、「閉じたタブローの探索」のセクションで説明されているように、タブローの空間を探索することで見つけることができます。この探索中、連結性によって拡張の選択肢の一部が排除されるため、探索が軽減されます。言い換えれば、ツリーのノード内のタブローは一般に複数の異なる方法で拡張できますが、連結性によって拡張できる方法が限られるため、さらに拡張する必要のある結果として得られるタブローの数が減少します。

これは次の（命題的な）例で見ることができる。鎖で構成されたタブロー${\displaystyle true-a}$節のセットについて${\displaystyle \{a,\neg a\lor b,\neg c\lor d,\neg b\}}$一般的には、4 つの入力句のそれぞれを使用して展開できますが、接続では、使用する展開のみが許可されます。${\displaystyle \neg a\lor b}$これは、タブローの木は一般には4つの葉を持つが、連結性を課すと1つしか持たないことを意味する。つまり、連結性によって、一般には考慮すべき4つのタブローではなく、拡張を試みるタブローは1つだけになる。選択肢がこのように減少するにもかかわらず、完全性定理によれば、集合が充足不能な場合は閉じたタブローを見つけることができる。

連結条件を命題（節）の場合に適用すると、結果として得られる計算体系は非合流的になる。例として、${\displaystyle \{a,b,\neg b\}}$満たされないが、適用すると${\displaystyle (C)}$に${\displaystyle a}$チェーンを生成する${\displaystyle true-a}$これは閉じられておらず、強い連結性または弱い連結性のいずれにも違反することなく他の拡張規則を適用することはできません。弱い連結性の場合、ルートの拡張に使用される節が充足不能性に関係している、つまり節の集合の最小充足不能部分集合に含まれている場合に限り、合流性が成立します。残念ながら、節がこの条件を満たすかどうかを確認する問題自体が難しい問題です。合流性がない場合でも、上記の「閉じたタブローの探索」のセクションで説明したように、探索を使用して閉じたタブローを見つけることができます。探索は必要になりますが、連結性によって拡張の選択肢が減るため、探索はより効率的になります。

タブローは、同じ分岐内でリテラルが2回出現しない場合に正規である。この条件を適用することで、タブロー展開の選択肢を減らすことができる。なぜなら、非正規タブローを生成する節は展開できないからである。

しかし、これらの許可されていない展開手順は役に立ちません。${\displaystyle B}$リテラルを含むブランチです${\displaystyle L}$、 そして${\displaystyle C}$展開が規則性に違反する節である場合、${\displaystyle C}$を含む${\displaystyle L}$タブローを閉じるには、とりわけ、次の枝を展開して閉じる必要があります。${\displaystyle B-L}$、 どこ${\displaystyle L}$2 回発生します。ただし、このブランチの式は、${\displaystyle B}$単独で。結果として、閉じる同じ拡張ステップ${\displaystyle B-L}$また近い${\displaystyle B}$これは拡大することを意味します${\displaystyle C}$不要だった。さらに、もし${\displaystyle C}$他のリテラルが含まれていた場合、その展開によって閉じる必要のある他の葉が生成されます。命題論理の場合、これらの葉を閉じるために必要な展開は全く役に立ちません。一階述語論理の場合、いくつかの単一化のためにタブローの残りの部分にのみ影響を与える可能性があります。ただし、これらはタブローの残りの部分を閉じるために使用される置換と組み合わせることができます。

異なる世界を参照する数式が誤って相互作用するのを回避する方法の一つは、ブランチ内のすべての数式が同じ世界を参照するようにすることです。この条件は、整合性チェックの対象となるセット内のすべての数式が同じ世界を参照していると想定されるため、最初は真となります。ブランチを展開する際には、2つの状況が考えられます。新しい数式がブランチ内の他の数式と同じ世界を参照する場合と、そうでない場合です。前者の場合、ルールは通常通り適用されます。後者の場合、新しい世界でも成り立たないブランチ内のすべての数式はブランチから削除され、古い世界に関連する他のすべてのブランチに追加される可能性があります。

例えば、S5ではすべての数式が${\displaystyle \Box A}$ある世界で真であるということは、アクセス可能なすべての世界でも真である（つまり、アクセス可能なすべての世界では両方とも${\displaystyle A}$そして${\displaystyle \Box A}$（真実である）。したがって、適用する際には${\displaystyle {\frac {\neg \Box B}{\neg B}}}$異なる世界でもその結果が成り立つので、ブランチからすべての式を削除しますが、すべての式を保持することができます。${\displaystyle \Box A}$これらの式は新世界においても同様に成り立つ。完全性を保つため、削除された式は、旧世界を参照している他のすべての分岐に追加される。

異なる世界を参照する数式間の正しい相互作用を保証する別のメカニズムは、数式からラベル付き数式に切り替えることです。${\displaystyle A}$と書く人もいるだろう${\displaystyle w:A}$明確にするために${\displaystyle A}$世界で保持されている${\displaystyle w}$。

すべての命題展開規則は、すべて同じ世界ラベルを持つ式を参照すると述べることで、この変種に適合します。たとえば、${\displaystyle w:A\land B}$ラベルの付いた 2 つのノードを生成します${\displaystyle w:A}$そして${\displaystyle w:B}$; ブランチは、同じ世界の反対のリテラルが 2 つ含まれている場合にのみ閉じられます。${\displaystyle w:a}$そして${\displaystyle w:\neg a}$; 2 つのワールドラベルが異なる場合、クロージャは生成されません。${\displaystyle w:a}$そして${\displaystyle w':\neg a}$。

様相展開規則は、異なる世界を参照する結果をもたらす可能性がある。たとえば、${\displaystyle \neg \Box A}$次のように書かれる

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

この規則の前提条件と帰結は世界を参照する${\displaystyle w}$そして${\displaystyle w'}$それぞれ。さまざまな計算式は、ラベルとして使用される世界のアクセス可能性を追跡するために異なる方法を使用します。いくつかは次のような擬似式を含みます。${\displaystyle wRw'}$示すために${\displaystyle w'}$からアクセスできます${\displaystyle w}$. 他のいくつかは、整数のシーケンスをワールドラベルとして使用し、この表記法はアクセス可能性関係を暗黙的に表しています（たとえば、${\displaystyle (1,4,2,3)}$からアクセスできます${\displaystyle (1,4,2)}$）

異なる世界で成り立つ数式間の相互作用の問題は、集合ラベル付けタブローを用いることで克服できる。これは、ノードに数式の集合がラベル付けされたツリーであり、展開規則は、葉のラベルのみに基づいて（枝内の他のノードのラベルには基づかずに）、新しいノードを葉に接続する方法を説明する。

様相論理のタブローは、与えられた様相論理における一連の様相論理式の充足可能性を検証するために使用されます。一連の式が与えられた場合、${\displaystyle S}$モデルの存在を確認する${\displaystyle M}$そして世界${\displaystyle w}$そのため${\displaystyle M,w\models S}$。

展開規則は、使用する特定の様相論理に依存する。基本様相論理Kのタブローシステムは、命題タブロー規則に次の規則を追加することによって得られる。

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

直感的に言えば、この規則の前提条件は、すべての公式の真偽を表している。${\displaystyle A_{1},\ldots ,A_{n}}$すべてのアクセス可能な世界において、そして真実${\displaystyle \neg B}$いくつかのアクセス可能な世界では。この規則の結果、そのような世界の1つで真でなければならない式が存在します。${\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'}$: 同じモデルだが、異なる世界が存在する可能性がある。セットラベル付きタブローは、各式が真であると仮定される世界を明示的に追跡しない。2つのノードが同じ世界を参照する場合もあれば、そうでない場合もある。ただし、任意のノードにラベル付けされた式は、同じ世界で真であると仮定される。

数式が真であると仮定される世界が異なる可能性があるため、ノード内の数式は、その子孫ノードすべてにおいて自動的に有効になるわけではありません。なぜなら、様相規則を適用するたびに、ある世界から別の世界への移動に対応するからです。この条件は、集合ラベル付けタブローによって自動的に捉えられます。拡張規則は、適用される葉ノードのみに基づいており、その祖先ノードには基づかないためです。

特に、${\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\to 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 )}$これにより、モーダル展開ルールの前にのみ適用され、他のルールを適用不能にする式のみが削除されます。この条件は、2 つのルールを 1 つのルールに統合することによっても定式化できます。結果として得られるルールは、古いルールと同じ結果を生成しますが、古いルールを適用不能にするすべての式を暗黙的に破棄します。この削除メカニズム${\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\land \neg \Box a)}$: 適用される規則は順不同です${\displaystyle (T),(\land ),(\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\land Q)\}}$伴う${\displaystyle \neg \Box Q}$グローバルには成り立つがローカルには成り立たない。ローカル含意は、2 つの世界からなるモデルでは成り立たない。${\displaystyle P}$そして${\displaystyle \neg P,Q}$それぞれ真であり、2番目は1番目からアクセス可能である。最初の世界では仮定は真であるが${\displaystyle \neg \Box Q}$これは偽です。この反例が機能するのは、${\displaystyle P}$ある世界では真とみなされ、別の世界では偽とみなされることがある。しかし、同じ仮定がグローバルであるとみなされる場合、${\displaystyle \neg P}$モデルのどの世界においても許可されていません。

これら2つの問題は組み合わせることができ、${\displaystyle B}$は、${\displaystyle A}$世界的な仮定の下で${\displaystyle G}$タブロー計算では、参照する世界に関係なく、すべてのノードに追加することを許可するルールによって、グローバルな仮定を扱うことができます。

タブロー展開ルールを記述する際、式は慣例に従って表記されることが多く、例えばαは常に次のように表される。${\displaystyle \alpha _{1}\land \alpha _{2}}$以下の表は、命題論理、一階述語論理、様相論理における論理式の表記法を示しています。

最初の列の各ラベルは、他の列のいずれかの数式として扱われます。上線付きの数式は、${\displaystyle {\overline {\alpha _{1}}}}$は、${\displaystyle \alpha _{1}}$は、その場所に現れる式の否定です。たとえば、式では${\displaystyle \neg (a\lor b)}$サブフォーミュラ${\displaystyle \alpha _{1}}$はの否定です。

各ラベルは複数の等価な式を示すため、この表記法を用いることで、これらの等価な式すべてに対して単一の規則を記述することが可能になります。例えば、連言展開規則は次のように定式化されます。

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