2015年度情報論理学第 1回講義

2015 年度情報論理学第 1 回講義
2015 年 4 月 14 日 (火)
青戸等人 (東北大学電気通信研究所)
目次
-
講義の情報
はじめに ∼論理とは∼
論理学概観 ∼論理学の歴史を振り返りながら ∼
講義概要
1
情報論理学講義情報 (1)
講義の進め方
プリント教材あり．
講義ホームページよりダウンロード可能．
演習問題あり．
講義と間をおかずに復習するのが望ましい．期末試験
は演習問題を解いておけば解ける程度の難易度．
教科書・参考書
教科書：なし
参考書：
前原昭二著「記号論理入門」 (日本評論社)
小野寛晰著「情報科学における論理」 (日本評論社)
2
その他の (英語の) 参考書
定評のある参考書は前出の小野先生の本の最後を参照．
• 講義の内容に近い参考書： Dirk van Dalen, Logic and
Structure (3rd ed.), Springer-Verlag, 1991.
• トピックも広く書き方も非常に優れた参考書 (ただ
し，数学書の読み方に慣れていないと難しい )： Herbert B.
Enderton, A Mathematical Introduction to Logic (3rd
ed.), Academic Press, 2001.
• プログラムを使って説明している本 (プログラム好きの
人には良いかも )： John Harrison, Handbook of Practical
Logic and Automated Reasoning, Cambridge University
Press, 2009.
3
情報論理学講義情報 (2)
ホームページ
http://www.nue.riec.tohoku.ac.jp/
user/aoto/lecture/15Logic/
(講義資料や連絡など．随時更新予定)
オフィスアワー
[email protected] までメールで予約．
成績評価の方法
主に期末試験の結果によって評価する．ノート・資料・参
考書持ち込み可 (iPad,PC 等は不可)，再試験は行わない．
出席確認や復習問題の解答提出を課した場合，出席点と
して評価する．
4
目次
-
講義の情報
はじめに ∼論理とは∼
論理学概観 ∼論理学の歴史を振り返りながら ∼
講義概要
論理学とは
論理学は「推論の方法とその正しさ」についての学問．
「真な論理式とは，論理的な推論に従って導かれる論理
式のことである．」
どのように論理的な推論に従って導かれたかを示すもの
を証明とよぶ．
ここでいう論理，この講義で学習する論理は，より厳密
には数理論理学とよばれるもの．より幅広い論理学の文脈
では，論理的な推論は演繹的推論とよばれる．
5
社会現象
自然現象
理論
数学
論理
6
+---------+
| "理論" |
+----+---------+----+
|
数学
|
+-----+-------------------+------+
|
論理学
|
-----+--------------------------------+----さまざまな場面で，理論的な解析を使うことがあるが，
その道具は数学．数学のどのような分野を用いるかはいろ
いろだが (あるいは， “数学” には通常含まれてないような
分野かもしれない．オートマトン，アルゴリズム，プログ
ラム意味論， etc.)，数学をきちんと使いこなすには，数学
の基礎となる論理学 (論理的な推論の理解とやり方，数学の
仕組み・証明の仕方) を身につける必要がある．
7
論理的な推論 (Logical Reasoning) とは
何か物事が正しいと判断するまでには，いろいろな理由
がある．
• 両親や先生から教えられた
• 観察・分析の結果
• さまざまな科学的な実験結果との整合性がとれている
8
9
10
論理的な推論とは
• 推論方法の『根本』に焦点
• 絶対確実な推論のみ
• 後に正しくなくなるようなことがあるものは対象外
11
論理的な推論とは
論理的な推論の例：
「すべての人は死ぬ．
ソクラテスは人である．
従って，ソクラテスは死ぬ．」
「すべての鳥は嘴をもつ．
ペンギンは鳥である．
従って，ペンギンは嘴をもつ．」
これらの， 2 つの前提から 1 つの結論を導いている際に
使っている推論が論理的な推論の例．
12
論理的な推論とは
これらの推論はどれも
「すべての X は Y である．
a は X である．
従って， a は Y である．」
のような一般形をもつ．
論理的な推論とは，個々の言明の内容ではなく，言明の
一般的な形に基づく推論
13
論理的な推論
論理的な推論ではない例：
「すべての人は死ぬ．
ソクラテスはギリシャ人である．
従って，ソクラテスは死ぬ．」
導かれている結論は正しいが，論理的な推論ではない．
なぜなら，結論の正しさは，『ソクラテス』や『死ぬ』といっ
た内容に依存しているから．
14
論理的な推論
「すべての人は死ぬ．
ソクラテスはギリシャ人である．
従って，ソクラテスは死ぬ．」
この場合は，少し推論ステップを補足することで正しい
論理的な推論にすることが出来る．
「すべての人は死ぬ．
すべてのギリシャ人は人である．
ソクラテスはギリシャ人である．
従って，ソクラテスは死ぬ．」
数学のすべての命題は，このような正しい論理的な推論
によって得られる．
15
「
「
「
「
有限個の開集合の共通部分は開集合である」
ラムダ計算は合流性をもつ」
集合 A と B が可算であればその直積も可算である」
任意の帰納的部分順序集合は極大元をもつ」
これらは現代的な数学で意味のある命題．ほとんどの人
には，これらの命題のほとんどはおまじないのように意味
をもたないかもしれない．
さまざまな用語の定義はその分野を勉強しないとわから
ないが，用いる論理的な推論はすべて共通．どのような命
題も論理的な推論ステップを 1 つ 1 つ辿ることで示せる．
16
日本の初等教育で論理的な推論を鍛える代表選手は，中
学の幾何の問題．
A
D
O
B
C
|AB| = |DC| かつ |AC| = |DB| とするとき，
(1) △ABC と △DCB が合同であることを示せ．
(2) △ABO と △DCO が合同であることを示せ．
17
三角形の合同条件：
(a) 3 辺の長さがそれぞれ等しい．
(b) 2 辺の長さとその間の角がそれぞれ等しい．
(c) 1 辺の長さとその両端の角がそれぞれ等しい．
つまり，以下のような推論が正しい
「 3 辺の長さがそれぞれ等しい ⇒ 2 つの三角形は合同」
「 2 辺の長さとその間の角がそれぞれ等しい ⇒ 2 つの三角
形は合同」
「 1 辺の長さとその両端の角がそれぞれ等しい ⇒ 2 つの三
角形は合同」
18
推論ステップを 1 つ 1 つ辿ることで示せる．
(仮定より ) |AB| = |DC| かつ |AC| = |DB| (1)
(等号の性質より ) |BC| = |BC| (2)
((1),(2) と合同条件 (a) より ) △ABC と △DCB が合同 (3)
((3) と合同性の性質より ) |AB| = |DC| (4)
((3) と合同性の性質より ) ∠OAB = ∠ODC (5)
((3) と合同性の性質より ) ∠ABC = ∠DCB (6)
((3) と合同性の性質より ) ∠ACB = ∠DBC (7)
((6),(7) と減算の性質より )
∠ABO = ∠ABC − ∠DBC
= ∠DCB − ∠ACB = ∠DCO (8)
((5),(6),(8) と合同条件 (c) より ) △ABO と △DCO が合同
19
20
「言葉とルールがある」
※ ルールを知らないときちんとゲームはできない．
※ ゲームで使われる言葉を知らないとルールは理解できな
い．
21
「言葉とルールがある」
※ ルールを知らないときちんとゲームはできない．
※ ゲームで使われる言葉を知らないとルールは理解できな
い．
「数学的な考え方を身につければ数学は出来る．」
「論理学は数学の言葉でありルールである」
※ 「証明ができるようになるには数学的な考え方がわかれ
ばよい」かもしれないが，論理学の言葉とルールをきちん
と知れば数学の証明が*きちんと *出来る．
「意見や見解の相違」に終わってしまう議論ではなく，
「何が正しく (証明がある )，何が正しくなく (反例がある )，
何が未解決問題なのか」の白黒がつくのが，理論．
22
なぜ論理学を学ぶのか
「知っている」
———————
• 人が言っているか
ら．．．
• 教科書に書いてあ
るから．．．
• 先生が言うから．．．
≪
「知っている」
———————
• その結論が出てくる
までの，仮定と推論過
程を辿ることができる
• 実験事実と理論的な
仮定の区別ができる
• 実験事実や理論的な
仮定と， (まだわかって
いない ) 真実との区別が
できる
23
目次
-
講義の情報
はじめに ∼論理とは∼
論理学概観 ∼論理学の歴史を振り返りながら ∼
講義概要
(お断り ) 以下で紹介する歴史の話は，講義内容を俯瞰するための参考に紹介する
ものであり，史実の確かさについて保証するものではありません．
23
アリストテレス論理学
論理学の始まりといわれているのはギリシャのアリスト
テレス (Aristotle, B.C.384–322)．
「すべての人は死ぬ．
ソクラテスは人である．
従って，ソクラテスは死ぬ．」
アリストテレス論理学はその後 17 世紀まで論理学の基礎
であった．
24
アリストテレス論理学
アリストテレスは，以下の 4 つのタイプの言明について，
syllogism とよばれる推論がどのような場合に正しいか議
論した．
All X is Y
No X is Y
Some X is Y
Some X is not Y
25
アリストテレス論理学
以下は正しい論理的な推論か？
(1) All X is Y
Therefore, All non-Y is non-X
(2) All X is Y
No Z is Y
Therefore, No Z is X
(3) All X is Y
Some Z is Y
Therefore, Some Z is non-X
26
Venn Diagrams ベン図
(Venn, 1881) 論理的な推論はベン図を使うと考えやす
い．
A
27
Venn Diagrams ベン図
B
28
A と B の積 (共通部分)
A∩B
29
A と B の和 (合併)
A∪B
30
A の反転
A◦
31
B の反転
B◦
32
ド・モルガンの法則 (1)
(A ∪ B)◦ = A◦ ∩ B ◦
33
ド・モルガンの法則 (2)
(A ∩ B)◦ = A◦ ∪ B ◦
34
部分集合 (A ⊆ B)
B
A
A⊆B ⇔A∩B =A⇔A∪B =B
⇔ A ∩ B ◦ = 0 ⇔ A◦ ∪ B = 1
(ここで， 0 は空集合， 1 は全体集合を表す． )
35
アリストテレス論理学 (再)
前の推論 (2) をベン図を使って考えてみると？
All X is Y
No Y is Z
Therefore, No X is Z
X⊆Y
Y ∩Z =0
Therefore, X ∩ Z = 0
この推論にはどんな法則が使われているだろうか？
36
Algebra ’al-jabr’
Algebra(代数) というと現在では抽象代数を指すが，語
源はアラビア語の’al-jabr’：
式の変形によって等式の解を得る方法
1+x=3−x
⇒ 2x = 3 − 1
⇒ 2x = 3 − 1
⇒ x=1
37
Algebra ’al-jabr’
Algebra(代数) というと現在では抽象代数を指すが，語
源はアラビア語の’al-jabr’：
式の変形によって等式の解を得る方法
1+x=3−x
⇒ 2x = 3 − 1
⇒ 2x = 3 − 1
⇒ x=1
論理推論を式変形のように簡単にできないか．
37
X⊆Y
(1)
Y ∩Z =0
(2)
Therefore, X ∩ Z = 0
By
By
By
By
By
By
By
(1)
(3)
(2)
(4),(5)
(6)
(7)
(8)
X ∩Y◦ =0
X ∩Y◦∩Z =0
X ∩Y ∩Z =0
(X ∩ Y ∩ Z) ∪ (X ∩ Y ◦ ∩ Z) = 0
(X ∩ Z) ∩ (Y ∪ Y ◦) = 0
(X ∩ Z) ∩ 1 = 0
X ∩Z =0
(3)
(4)
(5)
(6)
(7)
(8)
38
ジョージ・ブール
(George Boole, 1815-1864)
(画像はウィキペディアより引用)
39
ブール代数
式変形にもとづく論理推論， “論理の代数”
A. De Morgan (Formal Logic, 1874), George Boole
(Calculus of Thought, 1854), C.S. Pierce, Ernst
Schr¨
oder (The Algebra of Logic, 1890), W.S.Jevons
(Pure Logic, 1864; Elementary Lessons in Logic, 1870).
1.
2.
3.
4.
5.
6.
X
X
X
X
X
X
∪X =X
∩X =X
∪Y =Y ∪X
∩Y =Y ∩X
∪ (Y ∪ Z) = (X ∪ Y ) ∪ X
∩ (Y ∩ Z) = (X ∩ Y ) ∩ X
40
7. X ∩ (X ∪ Y ) = X
8. X ∪ (X ∩ Y ) = X
9. X ∩ (Y ∪ Z) = (X ∩ Y ) ∪ (X ∩ Z)
10. X ∪ (Y ∩ Z) = (X ∪ Y ) ∩ (X ∪ Z)
11. X ∪ X ◦ = 1
12. X ∩ X ◦ = 0
13. (X ◦)◦ = X
14. X ∪ 1 = 1
15. X ∩ 1 = X
16. X ∪ 0 = X
17. X ∩ 0 = 0
18. (X ∪ Y )◦ = X ◦ ∩ Y ◦
19. (X ∩ Y )◦ = X ◦ ∪ Y ◦
41
数学のおける公理化
19 世紀後半になって数学のさまざまな概念に厳密な定義
が取り入れられるようになってきた．
非ユークリッド幾何学 (ロバチェフスキー (1829 年)，ボー
ヤイ (1832)) とユークリッド幾何学・非ユークリッド幾何
学の公理化
直線上の点は「互いに触れ合う 2 片の境界」により確定され
る (アリストテレス )
⇒ 切断による実数の定義 (Dedekind, 1872)
⇒ 有理数のコーシー列による実数の定義 (Cantor, 1883)
集合にもとづく自然数論の公理化 (Dedekind, 1888)
ユークリッド幾何の公理 ⇒ ヒルベルトの公理 (Hilbert,1899)
42
記号の導入と命題の形式化
Peano による Formulario mathematico プロジェクト：
「論理学や数学に記号を取りいれ，すべての知られてい
る数式や定理を記述できる標準的な数学の書式を作ろう．」
• ∩， ∪， ∈， ⊆ などの記号を導入．
• Formulario mathematico (1895 に初版を出版， 1908
に第 5 版を出版)
’al-jabr’ のプリンシプルを数学のもっと広い範囲へ
43
ジュゼッペ・ペアノ
(Giuseppe Peano, 1858–1932)
(画像はウィキペディアより引用)
44
フレーゲによる論理学の刷新
1884 年『算術の基礎』
1893 年『算術の基本法則』第 1 巻
1903 年『算術の基本法則』第 2 巻
「論理に基づいてどこまで数学が展開できるのだろうか」
多く
•
•
•
•
の革新的なアイデアで現代の論理学の基礎を構築
真理値 (真と偽) の導入
関数と引数に分解した命題の導入
論理変数と量化子の導入
証明体系の導入
45
アリストテレス論理学を一般化
「すべての人は死ぬ．
ソクラテスは人である．
従って，ソクラテスは死ぬ．」
「 ∀x (P x → Q x) ⇒ P a ⇒ Q a」
当時の数学を展開できる論理の体系を与えたように見え
たが，その体系には矛盾があることが判明 (ラッセルのパラ
ドックス )．
アイデアも記法も非常に難解であったため，その仕事は
なかなか知られることがなかった．
46
ゴットロープ・フレーゲ
(Gottlob Frege, 1848 − 1925)
(画像はウィキペディアより引用)
47
ラッセルのパラドックス
”Hardly anything more unfortunate can befall a scientific writer than to
have one of the foundations of his edifice shaken after the work is finished. This
was the position I was placed in by a letter of Mr. Bertrand Russell, just when
the printing of this volume was nearing its completion.”
「学問的著作に携わるものにとって．．．，自らの仕事を完
遂した後に，それが土台から揺るがされる事態に逢着する
ことほど望まらしからぬことはない．この巻の印刷が終わ
ろうとしていたそのときに，バートランド・ラッセル氏か
ら送られてきた手紙によって私が立たされることになった
のが，まさにそうした状況であった．」 (フレーゲ，『算術の基
本法則』第 2 巻，あとがき )
48
バートランド・ラッセル
(Bertrand Russel, 1872-1970)
(画像はウィキペディアより引用)
49
ラッセルのパラドックス (集合論バージョン )
集合は対象の集まりですが，対象として集合そのものを考えてよい．
このとき，普通，集合そのものは，それ自体の要素にはなっていま
せん．つまり， X ∈ X は成立していません．けれども，集合全部の集
合，などを考えると，集合全部の集合は集合ですから，それ自身の要素
になっています．
今， A として自分自身を含まない集合を全部集めた集合をとります．
つまり， A というのは， X ∈
/ X が成立しているような X を集めた集合
です．このとき， A ∈ A か考えてみます． A ∈ A とすると，集合 A の定
義から， A ∈
/ A となっているはずで，これは矛盾ですから， A ∈ A は
成立していません．一方， A ∈
/ A とすると，集合 A の定義から， A は集
合 A に含まれるはずです．つまり， A ∈ A となってしまい，やはり矛盾
なので， A ∈
/ A も成立していません．従って， A ∈ A でも A ∈
/ A でも
ないことになってしまいます (？ )．
50
パラドックスの回避
自己言及的な構成を許すことが問題
型の理論 (theory of types)
(Bertrand Russel, 1903)
個体をタイプ 0 とする．
タイプ 0 の個体に対する述語をタイプ 1 とする．
タイプ 1 の述語に対する述語をタイプ 2 とする．
...
51
プリンキピア・マテマティカ
(Alfred North Whitehead and Bertrand Russell, 1910,
1912, and 1913)
「数学で発展させられた全てのアイデアと推論ステップ
を論理に基づいて厳密に再現しよう．」
フレーゲのアイデアと仕事がこれで知られるようになり，
数学に大きなインパクトを与えることになった．
52
短縮版の表紙
(画像はウィキペディアより引用)
53
プリンキピアの証明体系 (命題論理断片)
公理：
(1)
(2)
(3)
(4)
(5)
(P ∨ P ) → P
Q → (P ∨ Q)
(P ∨ Q) → (Q ∨ P )
(P ∨ (Q ∨ R)) → (Q ∨ (P ∨ R))
(Q → R) → ((P ∨ Q) → (P ∨ R))
推論規則：
A→B
B
A
A θ: 命題変数の具体化
Aθ
“公理から推論規則を繰り返し使って得らえるものだけ
が正しい命題”
54
真理値と真理値表
真理値：命題は真 (True) か偽 (False) の真理値を持つ．
真理値表： Wittgenstein, Emil Leon Post
命題論理断片では，証明体系にもとづく証明可能性は，
真理値 (真・偽) と真理値表によって説明できる． (命題論理
の完全性)
(Emil Leon Post, 1921)
プリンキピアの命題論理断片の証明システムと
真理値表で真になることが対応する．
55
エミール・レオン・ポスト
(Emil Leon Post, 1897-1954)
(画像はウィキペディアより引用)
56
ヒルベルトの計画
フレーゲ∼プリンキピア・マテマティカへの批判：型の
理論に基づくため，従来行われていたような数学の証明が
しづらい．
1904: 「論理学と算術の基礎」 (国際数学者会議での講演)
集合論や自然数論を形式化し，その無矛盾性を証明すべ
き．
1. プリンキピアの公理から本当に矛盾が導かれないか？
2. 数学のどんな定理の証明にも十分な証明体系は？
57
第一階述語論理
『数理論理学の基礎』 (Hilbert and Ackermann, 1928)
第一階述語論理，第二階述語論理， ... という形で，述語論
理を見通しよく整理．
公理：
(1) A → (B → A)
(2) (A → B) → ((A → (B → C)) → (A → C))
(3) A → (B → (A ∧ B))
(4) A ∧ B → A
(4’) A ∧ B → B
(5) A → A ∨ B
(5’) B → A ∨ B
(6) (A → C) → ((B → C) → (A ∨ B → C))
58
(7) (A → B) → ((A → ¬B) → ¬A)
(8) ¬¬A → A
(9) A(t) → ∃xA(x)
(10) ∀xA(x) → A(t)
推論規則：
A→B
B
A
A(a) → C
C → A(a)
∃xA(x) → C C → ∀xA(x)
ただし， a は C に出現しない．
Hilbert の問題提起
• 証明体系の無矛盾問題． (どうやって体系から矛盾が
導かれないということが示せるのか？ )
• 証明体系の完全性問題． (正しい論理式は必ず証明体
系をつかって示せるのだろうか？ )
59
第一階述語論理の完全性
(Kurt, G¨
odel, 1930)
第一階述語論理の証明体系と意味論が対応する．
従って，第一階述語論理の証明体系は無矛盾．
60
社会現象
自然現象
理論
数学
論理
61
理論
数学
論理
数学の理論は，論理を対象とすることもできる．
62
意味論
数学
論理
数学の理論は，論理を対象とすることもできる．
63
意味論
数学
論理
構文論
64
意味論と証明論
意味論：数学の概念を使って論理を調べる．
「真な論理式とは，すべての数学的なモデル上で成り立
つ論理式のことである．」
構文論：論理の立脚点．数学の基礎付け．
「真な論理式とは，論理的な推論に従って導かれる論理
式のことである．」
意味論と構文論における真の概念は等価なのか？
「意味論と証明論は論理学の両輪」
65
自然演繹法 (Natural Deduction)
(Gerhard Gentzen, 1935)
プリンキピアの証明体系や Hilbert&Ackermann の証明
体系 (ヒルベルト流の体系) は，実際の数学で使われる証明
のやり方とはかけはなれている．
⇒ 実際の数学の推論に即した証明体系の発明
66
証明図
自然演繹法では証明図を作ることによって証明を行う．
「すべての x について P x ならば Q x である．
P a である．
従って， Q a である．」
証明図
[∀x(P (x) → Q(x)]
P (a) → Q(a)
Q(a)
[P (a)]
(いくつかの) 推論規則を用いて証明図を記述．
横棒は 1 つの推論ステップを， [ ] は前提であることを示す．
67
ゲルンハルド・ゲェンツェン
(Gerhard Gentzen, 1909–1945)
(画像はウィキペディアより引用)
68
目次
-
講義の情報
はじめに ∼論理とは∼
論理学概観 ∼論理学の歴史を振り返りながら ∼
講義概要
情報論理学講義概要 (1)
講義の目的 (シラバスより )
数理論理学は，情報科学分野全般における数学的・理
論的な思考技術の基本として，更にまた，ソフトウェア科学
における形式的技法の基礎として重要である．このような
観点から，数理論理学の基礎を修得することを目的とする．
講義の概要 (シラバスより )
数理論理学の基本である命題論理および述語論理につ
いて，命題の形式化，命題の解釈法，トートロジー，論理
的同値性，形式的推論法，意味論，健全性と完全性などに
ついて講義する．
68
情報論理学講義概要 (2)
達成目標 (シラバスより )
・自然言語で与えられた命題を論理式を用いて形式化する
能力の習得．
・推論の形式化についての理解．
・数学的論証の過程を理解し，明示する能力の習得．
・基礎的な数学的構造において，与えられたモデル上にお
ける命題の真偽を議論する能力の習得．
・証明可能性と恒真性の同等性についての理解．
69
情報論理学講義概要 (3)
• 命題論理の意味論
• 帰納的定義
• 命題論理の構文論 (自然演繹法)
• 第一階述語論理の意味論
• 第一階述語論理の構文論 (自然演繹法)
• 健全性と完全性 (意味論と構文論の対応)
最も応用範囲が広く，最も基本的な数理論理学の基礎を身につける．構
文論では，主要な体系として，ヒルベルト流の体系/自然演繹法/シー
ケント計算があるが，この講義では自然演繹法に焦点をしぼる．
70
(補足) 論理学は先端的な研究で応用されていないの？
いくつかの主要な応用を挙げる：
(1) 対話的証明器
数学の証明を形式的に記述するソフトウェア．今まで人
間の手で書かれていた証明では大幅に省略されるが，これ
を計算機上で厳密に (プログラムのように ) 記述．バグのな
い証明が可能になるばかりでなく，推論システムの出力検
証やユーザー本位の定理証明への応用など．
(2) SAT/SMT ソルバー
計算困難な論理式の充足可能性を高速に解くソフトウェ
ア．高速に解けるとは限らないが，実は，人間が解きたい
問題はかなり高速に解けることが多い．さまざまな問題を71，
論理式等でエンコードして， SAT/SMT ソルバーを用いる
ことで，解を高速に発見することができる．
(3) モデルチェッカー
ソフトウェアのバグを見つけるのにさまざまな入力を試
すのではなく，どのように動作して欲しいか (仕様) を論理
を用いて記述し，プログラムの入力や実行を抽象化するこ
とでモデルを構築し，モデルが仕様を満たすかを検査する
ことで，あらゆる入力や動作で (その仕様について ) 問題が
ないかどうかを判定する．
情報＋論理を背景としたアプローチは， Logic in
Computer Science とよばれており，情報科学／情報工学
の基本的な分野の重要な柱の 1 つ．
72

Download Report