Microsoft PowerPoint - design-theory-6.pptx

設計学

6. 設計の論理によるモデル化 武田 英明 [email protected] http://www-kasm.nii.ac.jp/~takeda/ @design_theory

設計への論理的アプローチ

• 設計のモデル化 – 集合論的アプローチ（一般設計学） 分類を知識として，その上で設計を考える • 数学的に“よい”構造（各種の定理の導出） • ものとものの関係の取り扱いが難しい – 論理的アプローチ 論理式を知識として，その上で設計を考える • より複雑な構造（関係等）が扱える • 計算機での推論への足がかり • 数学的にはそれほど”美しくない”

論理学

• 命題論理 • 述語論理 • 参考文献 – 数理論理学入門、高崎金久（京都大学） http://www.math.h.kyoto-u.ac.jp/~takasaki/edu/logic/ – 前原昭二「記号論理学入門」（日本評論社）

命題論理

• 素命題：P, Q, R, … • 論理記号：∧（連言），∨（選言），￢（否定） ⇒（含意），⇔（同値） • 論理式：素命題と論理記号を組み合わせたも の – P∧Q – （P∧Q）∨￢（Q∧R)

命題論理

• 真理値 p ￢p t f f t p q p∧q p∨q p→q p⇔q t t t t t t t f f t f f f t f t t f f f f f t t

論理式の同値性

• 論理記号の同値関係 – p∨q ≡ ￢((￢p)∧(￢q)) – p∧q ≡ ￢((￢p)∨(￢q)) – p⇒q ≡ (￢p)∨q – p⇔q ≡ (p⇒q)∧(q⇒p)

妥当な論証の例

• 「太郎は家と学校に同時にいることはない．太郎は家にいる．だから太郎は 学校にはいない．」 前提：太郎は家と学校に同時にいることはない． （AかつB)でない 前提：太郎は家にいる A 結論：太郎は学校にいない Bでない • 反例を探す：前提２が真，結論が偽とするなら，Aが真かつBが真，とするなら （AそしてB)は真，ならば「（AそしてB）でない」は偽．すなわち反例となる • 真理表なら A B （AかつB) (AかつB)でない A Bでない 場合１ t t t f t f 場合2 t f f t t t 場合3 f t f t f f 場合4 f f f t f t

論理式の同値性

• 可換律：φ∧ψ ≡ ψ∧φ, φ∨ψ ≡ ψ∨φ • 結合律： (φ∧ψ)∧χ ≡ φ∧(ψ∧χ), (φ∨ψ)∨χ ≡ φ∨(ψ∨χ) • 分配律： (φ∧ψ)∨χ ≡ (φ∨χ)∧(ψ∨χ), (φ∨ψ)∧χ ≡ (φ∧χ)∨(ψ∧χ) • 吸収律：φ∧(φ∨ψ) ≡ φ, φ∨(φ∧ψ) ≡ φ • ⇒の別表現：φ⇒ψ ≡ (￢φ)∨ψ • ⇔の別表現：φ⇔ψ ≡ (φ⇒ψ)∧(ψ⇒φ) • 二重否定の除去：￢￢φ ≡ φ • ド・モルガンの法則： ￢(φ∨ψ) ≡ ￢φ∧￢ψ, ￢(φ∧ψ) ≡ ￢φ∨￢ψ • 対偶の法則：φ⇒ψ ≡ ￢ψ⇒￢φ

命題の真偽

• 論理式には常に（どんな解釈でも）真（または偽）のものがある． • ((p→q)∧(q→r))→(p→r) p q r p→q q→r(p→q)∧(q→r) p→r (1) t t t t t t t t t t f t f f f t t f t f t f t t t f f f t f f t f t t t t t t t f t f t f f t t ｆ f t t t t t t f f f t t t t t p q r ￢p ￢p→q(￢p→q)→r t t t f t t t t f f t f t f t f t t t f f f t f f t t t t t f t f t t f f f t t f t f f f t f t  (￢p→q)→r 恒真（妥当） _{恒偽（矛盾）} 充足可能 充足不能 いかなる解釈でも真 いかなる解釈でも偽

恒真性

• 論理式φが恒真である |= φと書く – トートロジーとも • 論理式φが恒偽である |= (￢φ）

論理式のモデル

• 論理式φの解釈とは論理式φに含まれる全 ての素命題に真理値を割り当てること。真理 値割り当て。 • 論理式φが真理値割り当て M に対して真で あるとき， 真理値割り当て M は論理式φを 充足する（あるいは 真理値割り当て M は論 理式φのモデルである）と言う． M |= φ • モデルがある論理式φは充足可能

意味論的演繹関係

• 意味的演繹関係とは、論理式の集合Γと論 理式ψに対して， Γを充足する任意の真理 値割り当て M がψも充足すること（すなわち M |=Γ ならば M |=ψ となること） Γ |= ψ • “Γが正しければψも正しい” • Γ = {φ₁, ..., φ_n} とすると Γ |= ψ は |= φ₁∧…∧φ_n⇒ψである

公理論と意味論

• 意味論：素命題に真理値を割り振ることで論 理式の真理値を決定する • 公理論：公理と推論規則から定理を証明する．

公理

• 公理 – (A1): P⇒(Q ⇒P) – (A2): (P ⇒(Q ⇒R)) ⇒((P ⇒Q) ⇒(P ⇒R)) – (A3): (￢P ⇒￢Q) ⇒((￢P ⇒Q) ⇒P) • 推論規則 – (B1): PとP ⇒Qが定理式であればQは定理式で ある

証明とは

• A が Γ={S₁，_{...，Sn}から導かれる」（Γ |- A)とは，} S_n = A であり， (1) S_iは 公理． (2) S_iが，有限個の表現 S_j(j < i) から直接導か れる． Γ の全ての元に関して (1) か (2) を満たすこと をいう． (直接導かれるとは，推論規則を１回だ け適用するということ．) • Γ |- A 仮定ΓからAは証明可能

演繹定理

• (Γ,A |- B) → (Γ |- A → B) Γが空集合の時，(A |- B) → (|- A → B)

例

• 例）|- A→Aの証明 – 1. A→((A→A)→A) A1においてP=A,Q=(A→A) – 2. (A→((A→A)→A))→((A→(A→A))→(A→A)) A2においてP=A,Q=(A→A),R=A – 3. ((A→(A→A))→(A→A)) 1と2とB1 – 4. A→(A→A) A1においてP=A,Q=A – A→A 3と4とB1 • 公理 – (A1): P⇒(Q ⇒P) – (A2): (P ⇒(Q ⇒R)) ⇒((P ⇒Q) ⇒(P ⇒R)) – (A3): (￢P ⇒￢Q) ⇒((￢P ⇒Q) ⇒P)

完全性定理

• |= A ⇔ |- A – A が恒真と A が 証明可能 は同値 – Aのトートロジーと定理は一致 • 健全性 – |- A ⇒ |= A • 完全性 – |= A ⇒ |- A

一階述語論理

• 素命題：p(t1, t2, t3, …) – 述語：p, q, r, … – 項：t1, t2, t3, … • 定数項：A, B, C, … • 変数項：x, y, z, … • 論理記号：∧，∨，￢，⇒，⇔ ∀（すべて），∃（ある） ∀_{x(p(x)⇒q(x)): 全てのxでp(x)⇒q(x)が成立} ∃_{x(p(x)⇒q(x)): あるxでp(x)⇒q(x)が成立}

演繹

• 演繹 – PとP ⇒Qが定理式であればQは定理式である • A∪F |-_σ Th – A: 公理系 – F: 事実 – Th: 定理群 • 演繹：公理系Aと事実Fから定理群Thを導出

帰納

• 帰納 – PとQが定理式であればP ⇒Qは定理式である • A∪F |-_σ Th – A: 公理系 – F: 事実 – Th: 定理群 • 帰納：事実Fから公理系Aと定理群Thを導出

アブダクション

• アブダクション – QとP ⇒Qが定理式であればPは公理式である • A∪F |-_σ Th – A: 公理系 – F: 事実 – Th: 定理群 • アブダクション：事実Fと定理群Thから公理系 Aを導出

演繹，帰納，アブダクション

• 演繹 – (B1): PとP ⇒Qが定理式であればQは定理式で ある • 帰納 – (B2): PとQが定理式であればP ⇒Qは定理式で ある • アブダクション – (B3): QとP ⇒Qが定理式であればPは定理式で ある

演繹，帰納，アブダクション

• 演繹 – (B1): PとP ⇒Qが定理式であればQは定理式で ある • 帰納 – (B2): PとQが定理式であればP ⇒Qは定理式で ある • アブダクション – (B3): QとP ⇒Qが定理式であればPは定理式で ある

演繹，帰納，アブダクション

• A∪F |-_σ Th – A: 公理系 – F: 事実 – Th: 定理群 • 演繹：公理系Aと事実Fから定理群Thを導出 • 帰納：事実Fから公理系Aと定理群Thを導出 • アブダクション：事実Fと定理群Thから公理系 Aを導出

悪構造問題

[Rittel1972] 1. 形式的な定義ができない 2. 形式化することは問題を解くこと 3. どこまでいったら最終解であるかわからない 4. 解は真偽ではなく，いいか悪いかで判断される 5. 問題の操作を全部数え上げることができない 6. 問題は違いによって記述され，その違いは多様な説明が可能 7. 問題は別の問題の兆候 8. 解をテストする方法はない 9. 一回限りである 10. すべての問題はユニークである 11. 問題の解決は問題解決する人に委ねられる．

Rittel, H. (1972) On the Planning Crisis: Systems

Analysis of the ‘First and Second Generations’. In Bedriftsokonomen. No. 8. pp. 390-396.

設計解 要求仕様

（論理からみた）設計過程の特徴

• 設計解のあいまい性 – 不完全性：解は順次詳細化され、完全になる。(３) – 複数解の存在：唯一の解があるとは限らない。(４) • 仕様のあいまい性 – 不完全性：仕様は設計開始時に全て決められているとは限ら ない。(１，２) – 変更可能性：仕様は設計過程において変更されうる。(2) • 知識のあいまい性 – 不完全性：知識は設計開始時に全て用意されているとは限ら ない。(5, 10, 11) – 変更可能性：知識は設計過程中で変化することがある。(6) – 非整合性：知識は互いに矛盾することがある。(11)

基本設定

• 論理式集合として表現 Ds:設計対象（設計解候補） P: 対象の性質、属性、挙動（要求仕様） K: 設計知識

入出力モデル

P

_K

Ds

設計解 要求仕様 ・重量を支える ・重量を変位に変換する ・… 要求仕様 設計 設計解

仮説推論

_{(アブダクション）モデル}

設計解 _要求仕様

P

K

_

Ds

事実 _理論理論₂ 3 観察 理論1 可能な 仮説 ・重量を支える ・重量を変位に変換する ・…

設計過程の論理的定式化

• 双方向推論 • 繰り返し推論 Ds: 設計解 P: 設計解の性質や挙動 Ko: ものに関する知識

P

K

_

Ds

アブダクション 演繹

アブダクション

• アブダクション 与えられた式を満たすと期待される仮説を得る行為 • 例 ばね(x) 比例（ｘ, 重量, 変位） 比例（ｘ, 重量, 変位） アブダクション ばね(x)

設計過程の論理的定式化

P K  Ds アブダクション 演繹 Ds2 Ds1 Dsfinal P_final P2 P3 P1 K₁におけるアブダクション2 3 Ds3 K₂におけるアブダクション K₁における演繹 K₂における演繹

設計例

1. 設計要求：文鎮の機能は机の上の紙を押さえる ことである． 押さえる（文鎮, 紙, 机), 下にある（紙、机） 2. 設計知識： ものを押さえるには力をかける必要 がある．重力は力として働く．文鎮は質量がある ので，重力がある 押さえる(x, y, z) <- 力をかける(x,y)∧動かない(z) ∧下にある(z,y) 力をかける(x, y) <- 重力がある(x)∧下にある(y,x) 重力がある(x) <- 質量(x)∧地球上(x) 3. 設計結果 質量(文鎮) ∧地球上(文鎮) ∧動かない(机)∧下にある (紙,文鎮) ∧下にある_(机,紙)

押さえる（文鎮, 紙, 机) 下にある（紙、机） 押さえる（文鎮, 紙, 机) 下にある（紙、机） 押さえる(x, y, z) <- 力をかける(x, y) ∧動かない(z) ∧下にある(y,z) P K _ Ds アブダクション R

⊃

演繹 力をかける(文鎮, 紙) 動かない(机) 下にある（紙、机） 押さえる（文鎮, 紙, 机) 力をかける(文鎮, 紙) 動かない(机) 設計知識 対象 性質 要求仕様 アブダクション 演繹 押さえる（文鎮, 紙, 机) 下にある（紙、机） 押さえる（文鎮, 紙, 机) 下にある（紙、机） 押さえる(x, y, z) <- 力をかける(x, y) ∧動かない(z) 力をかける(x, y) <- 重力がある(x) ∧下にある(y,x) 重力がある(文鎮) 下にある(紙,文鎮) 動かない(机) 押さえる（文鎮, 紙, 机) 力をかける(文鎮, 紙) 重力がある(文鎮) 下にある(紙,文鎮) 動かない(机) 下にある（紙、机） 設計知識 対象 性質 要求仕様 P K  Ds アブダクション R

⊃

演繹 アブダクション 演繹

押さえる（文鎮, 紙, 机) 下にある（紙、机） 押さえる（文鎮, 紙, 机) 下にある（紙、机） 押さえる(x, y, z) <- 力をかける(x, y) ∧動かない(z) 力をかける(x, y) <- 重力がある(x) ∧下にある(y,x) 質量(文鎮) 地球上(文鎮) 下にある(紙,文鎮) 動かない(机) 質量(文鎮) 地球上(文鎮) 下にある(紙,文鎮) 動かない(机) 押さえる（文鎮, 紙, 机) 下にある（紙、机） 力をかける(文鎮, 紙) 重力がある(文鎮) 設計知識 対象 性質 要求仕様 P K _ Ds アブダクション R

⊃

演繹 アブダクション 演繹 重力がある(x) <- 質量(x)∧地球上(x) （狭義の）設計解 利用環境など 解の持つ性質

設計過程の論理的定式化

• 矛盾の取り扱い • 知識の変遷 circumscription meta-level reasoning

Circumscriptionの利用

知識の記述は常に不完全 ＝ 矛盾の発生 例外を記述する項目を付加して、circumscriptionを行う 例外事項の算定 ＝ 矛盾の解消 新たな問題の発生 矛盾の解消と新たな問題提起 Rule1: ばね(x) ¬ab比例（x, 重量, 変位） Rule2:ばね(x) 過負荷(x) ¬ 比例（x, 重量, 変位） Circumscription abばね(x) 過負荷(x) Rule1' :ばね(x) ¬過負荷(x )比例（x, 重量, 変位）

Meta-level Reasoningの利用

対象知識の利用に関する推論 • 対象レベルの状態を観察して、次の行為を決定する 推論 • 対象レベルの状態 – 対象記述Ds、 性質的記述P、利用可能な知識Kの要素 – 矛盾 – 操作の履歴 • 対象レベルへの操作 – 対象記述Ds、 性質的記述P、知識Kの操作

Meta-level Reasoningの利用

• 例

「矛盾が起きたら、矛盾の解消を行う」

if (confict?) then (KB-circumscription) 「新しい仮説が提案されたら、それを展開して、評価する」 if (newly-add? assumptions) then ((select-related-KB)(deduction))

Meta-level Reasoningの利用

• アブダクションと演繹によるDsとPの詳細化 • サーカムスクリプションによるKの洗練 • メタレベル推論 によるK, Ds, Pの操作と推論の制御 P サーカムスクリプション アブダクション K Ds 演繹 メタレベル

Meta-level Reasoningの利用

O 演繹 Ka C アクションレベル推論 P Circumscription Deduction Abduction Ko Ds 対象レベル推論 対象レベルの状況 対象レベルの操作 Ka: 行動に関する知識 Ds: Design Solution

P: Properties and Behavior of Design Solution Ko: Knowledge on Objects

設計過程の論理による定式化

問題提起 展開 評価 決定 提案 Circum-scription Operation of formula アブダクション 演繹

設計サイクル

• どうやって二段のものを制御するか。（問題提起） • ... • 蓋がトグルになっているとよい（図A）。（提案1・展開） • 問題はどうやってトグルを取り付けるかだ。（評価→下位の問題提起） • ... • 図Bのようにドアのようなものをつけてはどうか。（提案2・展開） • 片側だけで支えるのは心許ない。（評価） • どういった力でタバコを保持するのか。（評価→下位の問題提起） – モータの力を使えばよいのでは。（提案） – モータは回しっぱなしにするのか。（評価） • トグル式の蓋のほうがいいみたい。（決定） Figure A Figure B

まとめ

• 設計プロセスを論理推論の枠組みで形式化 – 論理式の変遷による設計過程の表現 • 演繹とアブダクション – c.f. 科学的発見の論理 • メタレベルの推論 – サーカムスクリプション – 知識の変更 • 設計は2重のアブダクション – 設計解の発見 – 設計知識の発見