ここでは，原書にある例の続きである．
要求3
会議参加予定者には，会議開始の少なくとも3週間前までに期日と場所の通知を行うこと．
対応する様相論理記述
∀p: Person, m: Meeting
Holds(m) ∧ Intentded(p,m) ⇒ ◆≥3w Notified(p, m)
「mという会議を開き，かつ p が出席を意図しているならば，3週間以上前のどこかで，その会議の通知がある」というのが解釈である．
前回と同様に3Wという時間（間隔）を用いている．全称限量子は，全ての会議や参加者に関して，それが成り立つということを示している．
前提1
もし，会議の日付や場所が適切で，そのことが通知されるならば，会議参加予定者は，会議に出席する．
対応する様相論理記述
∀p: Person, m: Meeting
Intended(p,m) ∧ Notified(p, m) ∧ Convenient(m, p) ⇒ ◇ Participates (p, m)
会議自体は，未来のどこかなので，様相演算子「いつか」を使用している．開催日を過ぎた未来には，意味がない．
前提2
ミーティング場所が便利の良い場所であれば，その場所は恒に便宜が良い
対応する様相論理記述
∀p: Person, m: Meeting
Convenient(m, p) ⇒ □ Convenient (m, p)
そういう前提を置くと云うことである．
(nil)
ここでは，原書にある例を幾つか見る．
要求1
列車のドアは，プラットフォーム（駅）間では，閉まっていなければならない．但し，緊急事態のためにプラットフォーム間で停止している間は除く．
対応する様相論理記述
∀tr: Train, pl: Platform
（●At(tr, pl) ∧ ¬At(tr, pl) ⇒ tr.Doors = ‘closed’ W [At(tr, next(pl)) ∨ Alarm (tr) ∧ ¬Moving(tr)]）
「一つ前ではプラットフォームにいるが，いまはいない」というのが条件部分である．このとき，列車のドアは，「閉まっている．それは，列車が次の駅に到着するか，停止してアラームがあるときまで続く」というのが，この文の解釈である．
最初の束縛変数の定義部分（∀tr: Train, pl: Platform）は，これまで説明していない．集合の要素と捉えてもよいし，なじみの抽象データ型とインスタンスというとらえ方でも良い．いずれ説明したい．trというのはある列車を，plはあるプラットフォーム（駅）を示している．いま全称限量子で束縛しているので，一つ前に駅にいて，いまはその駅にいない列車という条件になっている．ある列車を考えたときに，全ての駅に同時に存在することはできないので，「前に」ある駅にいた列車がいまはいないという制約が，●At(tr,pl)の部分である．●で十分かは，議論があるだろうが，何らかの制約は必要になる．
要求2
列車は，次のプラットフォームに5分以内に到着しなくてはならない．
対応する様相論理記述
∀tr: Train, pl:Platform (At(tr, pl) ⇒ ◇≤5m At(tr, next(pl))
◇≤5mという記述法は，始めて出てきている．◇は，いつか生じるということである．いつかというのは，あまりにも漠としているので，制約を加えている．時間（間隔）制約を書くときには，比較的よく見る記法となる．論理的な取扱に関して，実践的な方法はすくない ．ここでは，あくまで要求としてどう表現するかというレベルで考える．
次回も引き続き原書の例について考える．
(nil)
最初は，操作（証明）を行う時に必要な公理である ．様相論理の場合は，少し複雑なので，「未来」における例を示す．
(0) □ φ → φ
(1) ○¬φ ⇔ ¬○φ
(2) ○(φ → ψ) ⇔ (○φ → ○ψ)
(3) □(φ → ψ) ⇔ (□φ → □ψ)
(4) □φ → □○φ
(5) (φ ⇒ ○φ) → (φ ⇒ □φ)
(6) φWψ ⇔ [ψ ∨ (φ ∧ ○(φWψ))]
(7) □φ ⇒ φWψ
ここで始めて出てきた φ ⇒ ψ は，□ (φ → ψ) である．また，φ ⇔ ψ は，□ (φ ↔ ψ) である．ほとんど，意味は明らかであろう．ちなみに□, ◇, U は，上記を用いて，次の様に代数的に書くことができる．
□φ⇔(φ∧○□φ)
◇φ ⇔ (φ ∧ ○◇φ)
φUψ ⇔ ( ψ ∨ [φ ∧ ○ (φUψ)]
次は，いつもの（証明）規則である．典型的なものを示す．
特殊化
□ φ ⊢ φ
全ての φ が真であれば，ある φ も真である．これは，公理(0)でもある．
MP (Modus Ponens)
(φ１ ∧ … ∧ φn） ⇒ ψ, □p1, …, □ φn ⊢ □ ψ
推移律
φ ⇒ ψ, ψ ⇒ ξ ⊢ φ ⇒ ξ
単調性
φ ⇒ ψ ⊢ □φ ⇒ □ψ
(nil)