タブロー計算
参考文献
戸次 大介; "数理論理学"
西村 祐輝; "Kripke Frameの性質とTableauの停止性"
T. Bolander, Patrick Blackburn; "Termination for hybrid tableaus"
T. Bolandar, Patrick Blackburn; "Termination teblaeu calculi for hybrid logics extending K"
メモ
古典命題論理のタブロー計算
および
古典述語論理のタブロー計算
$ \bf TAB
は
戸次 大介; "数理論理学"
に詳しい
様相論理のタブロー計算
命題動的論理
に関するのは
Malvin Gattinger
が
Lean 3
や
Lean 4
で形式化している
M. Gattinger; "A Verified Proof of Craig Interpolation for Basic Modal Logic via Tableaux in Lean"
https://malv.in/2022/AiML2022-basic-modal-interpolation-lean.pdf