计算机科学逻辑/时序逻辑

模态逻辑

模态逻辑通过对可能性和必要性模态的运算符扩展命题逻辑。这些基本的模态运算符通常写成 $\Box$（或L）表示必然，$\Diamond$（或M）表示可能。每个都可以用以下方式从另一个定义：

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