タブローの方法
提供: miniwiki
タブローの方法(英 tableau[1] method)とは、真理の木(truth tree)あるいは意味論的タブロー(semantic tableau)または分析タブロー(analytic tableau)と呼ばれるものを用いて、論証の妥当性や、論理式が矛盾しているかやトートロジーであるかを機械的に調べる判定手続き(decision procedure)の一種である。ヤーッコ・ヒンティッカらのモデル集合という考え方を応用して作られ、レイモンド・スマリヤンによって広められた。
方法
信頼性
タブローの方法は上記に示したような適切な規則を与えた場合、得られる結果は信頼できる。つまり常に正しい。
決定可能性
タブローの方法は命題論理や一引数の一階述語論理において決定可能である。つまり有限ステップで必ず判定を行える。しかし、多引数の一階述語論理において決定不可能である。つまり有限ステップで判定できない可能性がある。
参考文献
戸田山和久『論理学をつくる』pp92-107,126-131,185-201 名古屋大学出版会、2012年 ISBN 978-4-8158-0390-2
脚注
- ↑ 複数形はtableaux、もしくはtableaus。「タブローズ」と発音する。