計算機科學邏輯/時序邏輯

模態邏輯

模態邏輯透過對可能性和必要性模態的運算子擴充套件命題邏輯。這些基本的模態運算子通常寫成 $\Box$（或L）表示必然，$\Diamond$（或M）表示可能。每個都可以用以下方式從另一個定義：

$\Diamond P\leftrightarrow \lnot \,\Box \,\lnot \,P.$