時相論理
temporal logic、tense logic、time logic、時制論理、時閒論理
體系
Arthur Norman Prior の時相論理 (TL) 演算子
$ Px: "It was the case that..."$ \lang P\rang xとも書く
$ Fx: "It will be the case that..."$ \lang F\rang xとも書く
$ Gx: "It always will be the case that..."$ \lbrack P\rbrack xとも書く
$ Hx: "It always was the case that..."$ \lbrack F\rbrack xとも書く
$ Px\iff\neg H\neg x,$ \neg P\neg x\iff Hx
$ Fx\iff\neg G\neg x,$ \neg F\neg x\iff Gx
規則 N :$ \frac{\vdash x}{\vdash Gx},$ \frac{\vdash x}{\vdash Hx}
公理 K :$ G(x\to y)\to(Gx\to Gy),$ H(x\to y)\to(Hx\to Hy)
$ x\to GPx,$ x\to HF x
線形 (linear)
interval temporal logic (ITL)
duration calculus (DC)
計量時相論理 (metric temporal logic; MTL)
計量 interval 時相論理 (metric interval temporal logic; MITL)
signal 時相論理 (signal temporal logic)
timestamp temporal logic (TTL)
timed propositional temporal logic (TPTL)
hyper temporal logic (HyperLTL)
時閒正規表現 (timed regular expression)
property specification language (PSL)
區閒論理
分岐 (branching)
樣相μ計算 (modal μ-calculus)
$ \mu x.pは方程式$ x=pの最小不動點を計算する 時相量子論理 (temporal quantum logic。量子論理) history projection operator (HPO) formalism
時制 (tense)
相 (aspect)