意味解決ツリー

意味解決木は、プログラミング言語の意味を定義するために使用される木です。^[1]第一階述語論理における節の充足不可能性を示す理論的なツールとしてよく使用されています。^[2]

参考文献

1. Kundu, S (1986-12-01). 「ツリー解像度と一般化セマンティックツリー」. ACM SIGART国際シンポジウム「知能システムのための方法論」議事録. ISMIS '86. ノックスビル、テネシー州、米国: Association for Computing Machinery. pp.  270– 278. doi :10.1145/12808.12838. ISBN 978-0-89791-206-8. S2CID  17442587。
2. キム・チュンキュ; ニューボーン・モンティ (2003). ドンガラ・ジャック; ラフォレンツァ・ドメニコ; オルランド・サルヴァトーレ (編). 「競合的意味木定理証明器と解決法」 .並列仮想マシンとメッセージパッシングインターフェースの最近の進歩. コンピュータサイエンス講義ノート. 2840.ベルリン、ハイデルベルク: シュプリンガー: 227– 231. doi :10.1007/978-3-540-39924-7_33. ISBN 978-3-540-39924-7。