タブローの方法(英 tableau[1] method)とは、真理の木(truth tree)あるいは意味論的タブロー(semantic tableau)または分析タブロー(analytic tableau)と呼ばれるものを用いて、論証妥当性や、論理式矛盾しているかやトートロジーであるかを機械的に調べる判定手続き(decision procedure)の一種である。ヤーッコ・ヒンティッカらのモデル集合という考え方を応用して作られ、レイモンド・スマリヤンによって広められた。

方法

編集

信頼性

編集

タブローの方法は上記に示したような適切な規則を与えた場合、得られる結果は信頼できる。つまり常に正しい。

決定可能性

編集

タブローの方法は命題論理や一引数一階述語論理において決定可能である。つまり有限ステップで必ず判定を行える。しかし、二引数以上の一階述語論理において決定不可能である。つまり充足可能な場合(例えば∀x∃yR(x,y))、有限ステップで終了せず、延々と手続きが続く状況に陥ることがあるからである。

参考文献

編集

戸田山和久『論理学をつくる』pp92-107,126-131,185-201 名古屋大学出版会、2012年 ISBN 978-4-8158-0390-2

脚注

編集
  1. ^ 複数形はtableaux、もしくはtableaus。「タブローズ」と発音する。

外部リンク 

編集