タブローの方法(英 tableau複数形はtableaux、もしくはtableaus。「タブローズ」と発音する。 method)とは、真理の木(truth tree)あるいは意味論的タブロー(semantic tableau)または分析タブロー(analytic tableau)と呼ばれるものを用いて、論証の妥当性や、論理式が矛盾しているかやトートロジーであるかを機械的に調べる判定手続き(decision procedure)の一種である。ヤーッコ・ヒンティッカらのモデル集合という考え方を応用して作られ、レイモンド・スマリヤンによって広められた。 方法
基本的な手続き タブローの方法では、検証したい論理論証の「前提」と「結論の否定」を初期式（根）として設定し、ツリー（木）の形で展開を行う。各論理式に対して割当てられた展開規則を適用し、矛盾が生じた段階でその枝を「閉じる」ことで、論証の妥当性や式を満たす可能性を機械的に判定する。
全ての枝が閉じた場合、元の前提から結論が導かれる（論証が妥当である）ことが証明される。
展開規則（命題論理） 主に使用される命題論理の展開規則（数式表現）は以下の通りである。
連言（And）の展開 式 が真であるとき、同じ枝の下に直線的に展開する。
選言（Or）の展開 式 が真であるとき、枝を2つに分岐（分岐規則）させて展開する。
否定（Not）の展開 二重否定などは以下のように解消する。
含意（If-Then）の展開 式 は と同値であるため、以下のように分岐する。
終了条件と判定 閉じた枝（Closed branch）：ある枝の経路上に、ある論理式 とその否定 が同時に現れた場合、その枝は矛盾しているため「閉じる」とされる。ウィキテキストや表記上は、末尾に や を付記して示す。 開いた枝（Open branch）：これ以上適用できる展開規則がなく、かつ矛盾が出ないまま残った枝。 判定： すべての枝が閉じた場合：元の論証は妥当（トートロジー）である。 1つでも開いた枝が残った場合：その枝の経路が反例（式を充足する解釈）を示しており、論証は不妥当である。 信頼性 タブローの方法は上記に示したような適切な規則を与えた場合、得られる結果は信頼できる。つまり常に正しい。 決定可能性 タブローの方法は命題論理や一引数の一階述語論理において決定可能である。つまり有限ステップで必ず判定を行える。しかし、二引数以上の一階述語論理において決定不可能である。つまり充足可能な場合(例えば∀x∃yR(x,y))、有限ステップで終了せず、延々と手続きが続く状況に陥ることがあるからである。
参考文献 戸田山和久『論理学をつくる』pp92-107,126-131,185-201 名古屋大学出版会、2012年 ISBN 978-4-8158-0390-2
脚注
外部リンク 8.真理木による真理値分析 (山陽学園大学 論理学)