様相論理のタブロー計算
メモ
結構多くのことがわかっていないらしい．
西村 祐輝; "Kripke Frameの性質とTableauの停止性"
より．
https://drive.google.com/file/d/1PedHXXliF8uKF_iZrWgxKRzzcVTKWNJt/view
反射的
または
推移的
な
Kripkeフレーム
に対する
タブロー計算
は停止性を持つということがわかっている
T. Bolandar, Patrick Blackburn; "Termination teblaeu calculi for hybrid logics extending K"
M. C. Mayer; "A proof procedure for hybrid logic with binders, transitivity and relation hierarchies."
対称的
な
Kripkeフレーム
に対してはわかっていない．
$ \bf S4,S5
のための
Kripkeフレーム
に至っては全くわかっていない
メモ
Linh Anh Nguyen; "Analytic Tableau Systems and Interpolation for the Modal Logics KB, KDB, K5, KD5"
https://www.mimuw.edu.pl/~nguyen/B5SL.pdf
M. Fitting; "Proof Methods for Modal and Intuitionistic Logics"
や
R. Goré; "Tableau Methods for Modal and Temporal Logics"
などがある
F. Masacci; "Strongly analytic tableaux for normal modal logics"
は
ラベル付きタブロー計算
なるものを考えて
$ \bf K
と
$ \bf T,D,4,5,B
拡張について良い体系を手にれた
対称的
な様相論理すなわち
$ \bf B,5
を含む論理には課題があるらしい
M. Fitting; "Proof Methods for Modal and Intuitionistic Logics"
では
semi-analytic sequent-like tableau system
なるものを考えて
$ \bf KB,KDB,B,S5
に与えた．
しかし
analytic superformula property
なる性質を持たない
決定手続きを与えることすら出来ない
今日では
$ \bf B,KB4,K45,KD45,S5
に対する
analytic superformula property
を持った
sequent-like tableau system
があることが知られている
R. Goré; "Tableau Methods for Modal and Temporal Logics"
を見よ．
ただし
$ \bf KB,KDB,K5,KD5
には無かったので，この論文ではそられを与えたとされる．
ところで
Craigの補間定理
が
タブロー計算
より得られる．
様相論理のCraig補間定理
は例えば以下を参考にせよ．
D. Gabbay; "Craig’s interpolation theorem for modal logics"
M. Fitting; "Proof Methods for Modal and Intuitionistic Logics"
W. Rautenberg; "Modal tableau calculi and interpolation"
L. Maksimova; "Amalgamation and interpolation in normal modal logics"
Craigの補間定理
は
Beth Definability Theorem
の証明に用いられる．
オリジナルの
W. Craig; "Linear Reasoning. A new form of the Herbrand-Gentzen theorem"
なども参考にせよ．