タブローの方法

出典: フリー百科事典『ウィキペディア(Wikipedia)』
移動: 案内検索

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

方法[編集]

信頼性[編集]

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

決定可能性[編集]

タブローの方法は命題論理や一引数一階述語論理において決定可能である。つまり有限ステップで必ず判定を行える。しかし、多引数の一階述語論理において決定不可能である。つまり有限ステップで判定できない可能性がある。

参考文献[編集]

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

脚注[編集]

[ヘルプ]
  1. ^ 複数形はtableaux、もしくはtableaus。「タブローズ」と発音する。