タブロー法の謎の木

本日は大学の修論研究発表会でした．

何故タブロー法は変な木を生成するだけで充足可能性判定ができるんだろうかとずっと疑問に思っていたのですが、あの木は（与えられた論理式が充足可能なときは）論理式を充足するあるモデルそのものなんだそうです．様相論理版のタブロー法が生成した木を見てみるとそれがよく分かりました．