Upgrade to Pro — share decks privately, control downloads, hide ads and more …

時間に関する推論

Yuka Ezura
January 22, 2017
180

 時間に関する推論

Yuka Ezura

January 22, 2017
Tweet

Transcript

  1. 用途 •  談話理解 •  プランニング •  並列プログラムの設計 •  プログラムのチェック Always

    x != 0 Sometime x == 0 {x == y} implies {Next {x == y + 1}} {x == y} Until {y == 0} {x == 0} implies {Next {Always {x != 0}}} // xが0になるのは1回だけ Sometime {! this.isInterrupted()} // このスレッドは永久に割り込まれない 時相論理アサーションのサンプル
  2. 基本的な表現方法 「太郎が 6 時に起床した」 1.  起床 (6 時, 太郎) 2. 

    HOLD (6 時, 起床 (太郎)) 3.  TRUE (6 時, 起床 (太郎))
  3. HOLD 述語と様相オペレータ •  HOLD 述語を使用 – いつ何が生じたか – HOLD (6 時, 起床

    (太郎)) •  様相オペレータを使用 – 解釈に時間情報を含む – TRUE (6 時, 起床 (太郎)) – I, 6 時 |= 起床 (太郎)
  4. 状況論理 •  1963 年に John McCarthy (1927-2011) が提 唱 • 

    ゴール状態が行為の列により達成 •  状況と行為の関係を述語論理で記述 卵 卵 卵 卵
  5. ファクト •  状況 : ファクトの集合 •  ファクトを表す論理式の真偽値は状況に依存 •  has (行為者,

    フライパン, 状況 1) = False •  has (行為者, フライパン, 状況 2) = True 1 2 3 4 5 卵 卵 卵 卵
  6. 行為による状況の変化 移行先の状況 : result( p , δ, s) 行為者 状況

    行為 s result(p, get(fry_pan), s) 卵 卵 get(fry_pan)
  7. 教科書の例 •  最初の状況 : 金庫 sf の鍵 key を所持 • 

    行為 : opens(sf, key) •  結果 : – 状況は result(p, opens(sf, key), s) – 金庫は open の状態 •  has(p, key, s) ∧ fits(key, sf) ∧ at(p, sf, s) => open(sf, result(p, opens(sf, key), s))
  8. 時間の情報 •  F(π, s) : s 以降のある状況 s’ で π(s’)

    が成立 •  G(π, s) : s 以降の全ての状況 s’ で π(s’) が成立 •  P(π, s) : s 以前のある状況 s’ で π(s’) が成立 •  H(π, s) : s 以前の全ての状況 s’ で π(s’) が成立
  9. 時間情報の関数を用いた例 •  状況 s において、場所 x で雨が降っており、人 p が x

    の屋外にいれば、将来、p が濡れている状況 s’ が 存在する •  (∀x∀p∀s)(raining(x, s)∧at(p, x, s)∧outside(p, s)) => F(λs’.wet(p, s’), s) ( F(π, s) : s 以降のある状況 s’ で π(s’) が成立 )
  10. 記述方法 •  様相オペレータで記述 – GP : P は以後はずっと真である – FP : P

    は以後は真になることがある – HP : P は以前にずっと真であった – PP : P は以前に真であったことがある – ◦P : 次の時点で P が真 – P UNTIL Q : Q が 真 となるまで P は真であり続ける •  同値や公理が多数存在
  11. 同値関係 GP ≡ ¬F¬P – G: 以後ずっと真になる – F: 以後は真になることがある – ¬F¬P ⇒

    「以降は”¬ P が真”になることがある」ことはない ⇒ 以降は”¬ P が真”にずっとならない ⇒ 以降は” P が偽”にずっとならない ⇒ 以降は P がずっと真になる
  12. 同値関係 HP ≡ ¬P¬P – H: 以前ずっと真であった – P: 以前に真になることがあった – ¬P¬P ⇒

    「以前に”¬ P が真”になることがあった」ことはない ⇒ 以前に”¬ P が真”にずっとならなかった ⇒ 以前に” P が偽”にずっとならなかった ⇒ 以前に P がずっと真であった ≡ HP
  13. 公理 •  P ただし、P はトートロジー •  G(P → Q) →

    (GP → GQ) •  H(P → Q) → (HP → HQ) •  P → HFP •  P → GPP
  14. McDermo5 の時間論理 •  ステート : ある瞬間の世界の記述 •  時間 : 密なステートの集合

    •  ファクト : 真となるステートの集合 •  イベント : 生じている区間の全順序凸集合 ステート
  15. 記述 •  ファクト – A が B の上にある : (ON A

    B) – ステート s でA が B の上にある : (T s (ON A B)) •  イベント – ステート s1, s2 間でイベント e が生じる : (Occ s1 s2 e)
  16. イベントとファクトの因果関係 (ecause p e1 e2 rf i) •  p が区間

    i の間に偽となら なければ、イベント e1 の後 に イベント e2 が時間遅れ i で生じる •  ただし、イベント e1 の rf の 時点から時間を測定する (pcause p e q rf i r1) •  p が区間 i の間に偽となら なければ、イベント e の後 にファクト f が時間遅れ i で 成立し、r1 の間成立し続け る e1 e2 rf 区間 i e 区間 i 区間 r1 f
  17. イベントとファクトの因果関係(訂正) (ecause p e1 e2 rf i) •  p が区間

    i の間に偽となら なければ、イベント e1 の後 に イベント e2 が時間遅れ i で生じる •  ただし、イベント e1 の rf の 時点から時間を測定する (pcause p e q rf i r1) •  p が区間 i の間に偽とならな ければ、イベント e の後に ファクト q が時間遅れ i で成 立し、r1 の間成立し続ける •  ただし、イベント e の rf の時 点から時間を測定する e1 e2 rf 区間 i e rf 区間 i 区間 r1 q
  18. 具体例 1.  (ecause p e1 e2 rf i) (ecause Keg_Is_Dry,

    Lit_Fuse, Keg_Explode, 1, [30sec, 2min]) 2.  (pcause p e q rf i r1) (pcause always (KILL x) (DEAD x) 1 [0, 0] FOREVER) e rf 区間 i 区間 r1 q e1 e2 rf 区間 i
  19. 時間区間の間の関係 (I before J) ∧ (J meets K) ⇒ (I

    before K) X before Y Y aner X X ------ Y ------- X meets Y Y met_by X X -------- Y ------- X overlaps Y Y overlapped_by X X -------- Y ---------- X starts Y Y started_by X X ------ Y --------------- X during Y Y contains X X ------ Y ------------------- X finishes Y Y finished_by X X ------ Y ------------------- X equals Y Y equals X X ------ Y ------
  20. 部分区間での成立 •  プロパティ HOLDS (p, t) ⇔ (∀t’) In (t’,

    t) ⇒ HOLDS (p, t’) •  プロセス OCCURRING (p, t) → (∃t’) In (t’, t)∧OCCURING (e, t’) •  イベント OCCURS (e, t)∧In (t’, t) → ¬OCCURS (e, t’)
  21. 概念 •  因果関係 ECAUSE (e1, t1, e2, t2) •  行動

    •  意思 •  計画 •  知識 •  信念
  22. 定性推論 •  物理的な世界の挙動の変化に関する推論 •  例 石を上に投げる •  加速度 : ​↑2 x

    / ​↑2  = − •  速度 : x / = ​↓0 + * t •  最初の上昇速度は正 (+) •  途中で静止 (0) •  ある地点から速度が負 (-) [X]
  23. 定性値の計算 [X] [Y] [X] + [Y] [X] × [Y] +

    + + + + 0 + 0 + - ? - 0 + + 0 0 0 0 0 0 - - 0 - + ? - - 0 - 0 - - - +
  24. 表記 •  表記 –  速度 : x / ⇒ [x

    / ] = x –  加速度 : ​↑2 x / ​↑2  ⇒ [​↑2 x / ​↑2 ] = ​↑2 x –  ​↑ x / ​↑  ⇒ [​↑ x / ​↑ ] = ​↑ x •  Newton の法則 ⇒ 定性微分方程式 F = −× x/ ⇒ ​↑ F = −×​↑+1  •  例) 石を投げた瞬間 –  [x] = 0, x = + –  [F] = −× = −
  25. 挙動推定のルール •  [X] ≠ 0 なら次の区間でも [X] はそのまま •  [X]

    – 0 なら次の区間では [X] = δX •  [X] ≠ 0 で [X] = -δX なら次の瞬間は [X] = 0 •  [X] は + から –、または – から + へ変化する際に0 を経由す る •  定性値の遷移は定性方程式を満足するように変化する •  区間で [X] = 0 なら、その区間の間、ずっと 0 •  区間で [X] ≠ 0 なら、一定の区間 0 にならない
  26. 石の挙動の推定結果 [X] = 0 x = + ​↑2 x = -

    [X] = + x = + ​↑2 x = - [X] = + x = 0 ​↑2 x = - [X] = + x = - ​↑2 x = - [X] = 0 x = - ​↑2 x = - 瞬間 区間 区間 瞬間 瞬間
  27. 参考文献 •  新田克己. 知識と推論. サイエンス社, 2005, 159p •  J. MA

    and B. KNIGHT. Reified Temporal Logics: An Overview. cms2.gre.ac.uk/research/aigroup/Papers/aireview.doc (参照 : 2013-5-11) •  DREW MCDERMOTT. A Temporal Logic for Reasoning About Processes and Plans*. h5p://csjarchive.cogsci.rpi.edu/1982v06/i02/p0101p0155/ MAIN.PDF (参照 : 2013-5-12) •  Eric Allen. Javaコードの診断: Javaプログラミングにおけるアサー ションと時相論理. h5p://www.ibm.com/developerworks/jp/java/library/j-diag0723/ (参照 : 2013-5-12) •  Antony Galton. Temporal Logic. h5p://plato.stanford.edu/entries/logic-temporal/ (参照 : 2013-5-12) •  小野寛晰.情報科学における論理. 日本評論社, 1994, 297p •  戸田山和久. 論理学をつくる. 名古屋大学出版会, 2000, 433p
  28. 参考文献 (状況論理) •  MARQUIS Who’s Who. h5p://hawking1.agulin.aoyama.ac.jp:2344/profile/100002199313 (参照 2013-5-11) • 

    F. van Harmelen et al . Handbook of Knowledge Representaxon. 2008. h5p://ii.fmph.uniba.sk/~sefranek/kri/handbook/chapter16.pdf (参 照 2013-5-11) •  宮田公治. 「状況」「状態」「様子」およびその類義語群の意味分析. h5p://dspace.wul.waseda.ac.jp/dspace/bitstream/2065/29440/1/ KokugogakuKenkyuToSiryo_27_Miyata.pdf (参照 2013-5-11) •  人工知能学会. 人工知能学辞典. 共和出版株式会社, 2005, 946p