模態語義圖

模態語義圖是檢驗模態命題演算中公式的常真性的圖表。模態命題演算是經典命題演算的擴充。它們有許多相仿之處，如模態命題演算中公式的有效性定義，和經典命題演算中公式的有效性定義是相仿的，它們都是常真式。但相對應的條件並不全同，在模態命題演算的公式中，因為引入了模態運算元口（必然）、◇（可能）。在定義有效性時，需要引進可能世界。

在經典命題演算中，可以利用真值表方法去檢驗公式的常真性。對模態命題演算中公式的常真性，也可用圖表檢驗方法。它類似於經典命題演算中的簡化真值表方法。20世紀50年代後期，模態邏輯學家提出多種方法來判定一個模態命題演算中合式公式的常真性。著名的有克里普克語義圖和休斯一克雷斯韋爾語義圖。前者包括克里普克T語義圖、S4語義圖、S5語義圖等；後者包括休斯一克雷斯韋爾T語義圖、54語義圖、S5語義圖等。藉助語義圖可以證明模態命題演算系統的可靠性和完備性。