時相論理
時相論理では2種類の作用素を使用する。論理作用素と様相作用素(英語版)である。論理作用素は一般的な真理関数作用素である( ¬ , ∨ , ∧ , → {\displaystyle \neg ,\lor ,\land ,\rightarrow } )。線形時相論理や計算木論理で使用される様相作用素を以下に示す。
他の表現:
作用素 R は V で表記されることがある。
作用素 W は weak until を意味する。 f W g {\displaystyle fWg} は f U g ∨ G f {\displaystyle fUg\lor Gf} と等価である。
B( φ {\displaystyle \phi } ) が論理式(wff)であれば、単項作用素は全て論理式である。B( φ {\displaystyle \phi } ) と C( φ {\displaystyle \phi } ) が論理式であれば、二項作用素は全て論理式である。
論理体系によっては一部の作用素は表現できない。例えば、Temporal Logic of Actions では N 作用素は表現できない。