| 模态语义图 modal semantical tableaux 检验模态命题演算中公式的常真性的图表。模态命题演算是命题演算的扩充。它们有许多相仿之处，如模态命题演算中公式的有效性定义，和命题演算中公式的有效性定义是相仿的，它们都是常真式。但相对应的条件并不全同，在模态命题演算中的公式，一般具有模态算子L(必然)、M(可能)，在定义有效性时，需要引进可能世界。在命题演算中，可以利用真值表方法去检验公式的常真性。对模态命题演算中公式的常真性，也可用图表检验方法。它类似于命题演算中的简化真值表方法。20世纪50年代后期，模态逻辑学家提出多种方法来判定一个模态命题演算中合式公式常真性。著名的有克里普克语义图和休斯-克雷斯韦尔语义图。前者包括克里普克T语义图、S 4语义图、S 5语义图;后者包括休斯-克雷斯韦尔T语义图、S 4语义图、S 5语义图。借助语义图可以证明模态命题演算系统的可靠性和完备性。 |