設計学 6. 設計の論理によるモデル化武田英明 takeda@nii.ac.jp 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 t f p 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) でない B でない A 反例を探す : 前提 2が真, 結論が偽とするなら,Aが真かつBが真, とするなら (AそしてB) は真, ならば (AそしてB) でない は偽. すなわち反例となる 真理表なら A B (A かつ B) (A かつ B) でない A B でない 場合 1 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) r 命題の真偽 ((p q) (q r)) (p r) p q r p p q ( p q) r p q r p qq r (p q) (q r) p r (1) t t t f t t t t t t t t t t t t f f t f t t f t f f f t t f t f t t t f t f t f t t t f f f t f t f f f t f f t f t t t t t f t t t t t t t f t f t t f f t f t f f t t f f t t f t f f t t t t t t f f f t f t f f f t t t t t 論理式には常に ( どんな解釈でも ) 真 ( または偽 ) のものがある. いかなる解釈でも真 いかなる解釈でも偽 恒真 ( 妥当 ) 恒偽 ( 矛盾 ) 充足可能 充足不能 恒真性 論理式 φ が恒真である = φ と書く トートロジーとも 論理式 φ が恒偽である = ( φ)
論理式のモデル 論理式 φの解釈とは論理式 φに含まれる全ての素命題に真理値を割り当てること 真理値割り当て 論理式 φが真理値割り当て M に対して真であるとき, 真理値割り当て M は論理式 φを充足する ( あるいは真理値割り当て M は論理式 φのモデルである ) と言う. M = φ モデルがある論理式 φは充足可能 意味論的演繹関係 意味的演繹関係とは 論理式の集合 Γと論理式 ψに対して, Γを充足する任意の真理値割り当て M がψも充足すること ( すなわち M =Γ ならば M =ψ となること ) Γ = ψ Γが正しければψも正しい Γ = {φ 1,..., φ n } とすると Γ = ψ は = φ 1 φ 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 1,...,S n } から導かれる (Γ - A) とは, S n = A であり, (1) S i は公理. (2) S i が, 有限個の表現 S j (j < i) から直接導かれる. Γ の全ての元に関して (1) か (2) を満たすことをいう. ( 直接導かれるとは, 推論規則を 1 回だけ適用するということ.) Γ - 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 - σ A: 公理系 Th 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.
( 論理からみた ) 設計過程の特徴 設計解のあいまい性 不完全性 : 解は順次詳細化され 完全になる (3) 複数解の存在 : 唯一の解があるとは限らない (4) 仕様のあいまい性 不完全性 : 仕様は設計開始時に全て決められているとは限らない (1,2) 変更可能性 : 仕様は設計過程において変更されうる (2) 知識のあいまい性 不完全性 : 知識は設計開始時に全て用意されているとは限らない (5, 10, 11) 変更可能性 : 知識は設計過程中で変化することがある (6) 非整合性 : 知識は互いに矛盾することがある (11) 基本設定 論理式集合として表現 Ds: 設計対象 ( 設計解候補 ) P: 対象の性質 属性 挙動 ( 要求仕様 ) K: 設計知識
入出力モデル 要求仕様 設計 設計解 P K Ds 要求仕様 設計解 重量を支える 重量を変位に変換する 仮説推論 ( ) モデル 可能な仮説 事実 理論 3 理論 2 理論 1 観察 K Ds P 設計解 要求仕様 重量を支える 重量を変位に変換する
設計過程の論理的定式化 双方向推論 繰り返し推論 K Ds P 演繹 Ds: 設計解 P: 設計解の性質や挙動 Ko: ものに関する知識 例 与えられた式を満たすと期待される仮説を得る行為 ばね (x) 比例 (x, 重量, 変位 ) 比例 (x, 重量, 変位 ) ばね (x)
設計過程の論理的定式化 K Ds P Ds1 演繹 P1 K 1 における 2 Ds2 K 2 における Ds3 K 1 における演繹 P2 K 2 における演繹 3 P3 Dsfinal Pfinal 設計例 1. 設計要求 : 文鎮の機能は机の上の紙を押さえることである. 押さえる ( 文鎮, 紙, 机 ), 下にある ( 紙 机 ) 2. 設計知識 : ものを押さえるには力をかける必要がある. 重力は力として働く. 文鎮は質量があるので, 重力がある押さえる (x, y, z) <- 力をかける (x,y) 動かない (z) 下にある (z,y) 力をかける (x, y) <- 重力がある (x) 下にある (y,x) 重力がある (x) <- 質量 (x) 地球上 (x) 3. 設計結果質量 ( 文鎮 ) 地球上 ( 文鎮 ) 動かない ( 机 ) 下にある ( 紙, 文鎮 ) 下にある ( 机, 紙 )
K Ds 押さえる (x, y, z) <- 力をかける (x, y) 動かない (z) 下にある (y,z) 力をかける ( 文鎮, 紙 ) 動かない ( 机 ) 下にある ( 紙 机 ) 演繹 P R 演繹設計知識対象性質要求仕様 押さえる ( 文鎮, 紙, 机 ) 下にある ( 紙 机 ) 押さえる ( 文鎮, 紙, 机 ) 下にある ( 紙 机 ) 押さえる ( 文鎮, 紙, 机 ) 力をかける ( 文鎮, 紙 ) 動かない ( 机 ) 押さえる (x, y, z) <- 力をかける (x, y) 動かない (z) 力をかける (x, y) <- 重力がある (x) 下にある (y,x) K Ds 演繹設計知識対象性質要求仕様 重力がある ( 文鎮 ) 下にある ( 紙, 文鎮 ) 動かない ( 机 ) 演繹 P R 押さえる ( 文鎮, 紙, 机 ) 下にある ( 紙 机 ) 押さえる ( 文鎮, 紙, 机 ) 下にある ( 紙 机 ) 押さえる ( 文鎮, 紙, 机 ) 力をかける ( 文鎮, 紙 ) 重力がある ( 文鎮 ) 下にある ( 紙, 文鎮 ) 動かない ( 机 ) 下にある ( 紙 机 )
演繹設計知識対象性質要求仕様 押さえる (x, y, z) <- 力をかける (x, y) 動かない (z) 力をかける (x, y) <- 重力がある (x) 下にある (y,x) 重力がある (x) <- 質量 (x) 地球上 (x) K Ds 質量 ( 文鎮 ) 地球上 ( 文鎮 ) 下にある ( 紙, 文鎮 ) 動かない ( 机 ) 演繹 P R 押さえる ( 文鎮, 紙, 机 ) 下にある ( 紙 机 ) 押さえる ( 文鎮, 紙, 机 ) 下にある ( 紙 机 ) ( 狭義の ) 設計解 利用環境など 質量 ( 文鎮 ) 地球上 ( 文鎮 ) 下にある ( 紙, 文鎮 ) 動かない ( 机 ) 押さえる ( 文鎮, 紙, 机 ) 下にある ( 紙 机 ) 力をかける ( 文鎮, 紙 ) 重力がある ( 文鎮 ) 解の持つ性質 設計過程の論理的定式化 矛盾の取り扱い 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の操作 推論 (abduction, deduction, circumscription) の実行
例 Meta-level Reasoning の利用 矛盾が起きたら 矛盾の解消を行う if (confict?) then (KB-circumscription) 新しい仮説が提案されたら それを展開して 評価する if (newly-add? assumptions) then ((select-related-kb)(deduction)) Meta-level Reasoning の利用 メタレベル サーカムスクリプション K Ds P 演繹 と演繹によるDsとPの詳細化 サーカムスクリプションによるKの洗練 メタレベル推論によるK, Ds, Pの操作と推論の制御
Meta-level Reasoning の利用 アクションレベル推論 Ka C O Ka: 行動に関する知識 演繹 対象レベルの状況 対象レベルの操作 対象レベル推論 Ds: Design Solution P: Properties and Behavior of Design Solution Ko: Knowledge on Objects Abduction Circumscription Ko Ds Deduction P 設計過程の論理による定式化 問題提起 Operation of formula 演繹 提案展開 Circumscription 評価 決定
設計サイクル どうやって二段のものを制御するか ( 問題提起 )... 蓋がトグルになっているとよい ( 図 A) ( 提案 1 展開 ) 問題はどうやってトグルを取り付けるかだ ( 評価 下位の問題提起 )... 図 Bのようにドアのようなものをつけてはどうか ( 提案 2 展開 ) 片側だけで支えるのは心許ない ( 評価 ) どういった力でタバコを保持するのか ( 評価 下位の問題提起 ) モータの力を使えばよいのでは ( 提案 ) モータは回しっぱなしにするのか ( 評価 ) トグル式の蓋のほうがいいみたい ( 決定 ) Figure A Figure B まとめ 設計プロセスを論理推論の枠組みで形式化 論理式の変遷による設計過程の表現 演繹と c.f. 科学的発見の論理 メタレベルの推論 サーカムスクリプション 知識の変更 設計は 2 重の 設計解の発見 設計知識の発見