20/05/09 13:18:40 Mxr6sv2r.net
メモ
URLﾘﾝｸ(ja.wikipedia.org)
タブローの方法(英 tableau[1] method)とは、真理の木(truth tree)あるいは意味論的タブロー(semantic tableau)または分析タブロー(analytic tableau)と呼ばれるものを用いて、論証の妥当性や、論理式が矛盾しているかやトートロジーであるかを機械的に調べる判定手続き(decision procedure)の一種である。
ヤーッコ・ヒンティッカらのモデル集合という考え方を応用して作られ、レイモンド・スマリヤンによって広められた。
目次
1 方法
2 信頼性
3 決定可能性
URLﾘﾝｸ(en.wikipedia.org)
In proof theory, the semantic tableau (/ta?blo?, ?tablo?/; plural: tableaux, also called 'truth tree') is a decision procedure for sentential and related logics, and a proof procedure for formulae of first-order logic.
History
The method of semantic tableaux was invented by the Dutch logician Evert Willem Beth (Beth 1955) and simplified, for classical logic, by Raymond Smullyan (Smullyan 1968, 1995).
It is Smullyan's simplification, "one-sided tableaux", that is described above. Smullyan's method has been generalized to arbitrary many-valued propositional and first-order logics by Walter Carnielli (Carnielli 1987).[1]
Tableaux can be intuitively seen as sequent systems upside-down. This symmetrical relation between tableaux and sequent systems was formally established in (Carnielli 1991).[2]