計算機科学概論(応用編) 数理論理学を用いた自動証明

Presentation on theme: "計算機科学概論(応用編) 数理論理学を用いた自動証明"— Presentation transcript:

1 計算機科学概論(応用編) 数理論理学を用いた自動証明
計算機科学概論(応用編) 数理論理学を用いた自動証明 山本章博 情報学研究科 知能情報学専攻 （工学部 情報学科) 　　　

2 内容 “証明”する機械を人工的に作るために 2種類の論証 数理論理学 自動証明
人工知能(Artificial Intelligence)の視点から 2種類の論証 数理論理学 数学的な証明の例と分析 1970年代の高校数学 IIB を題材に 自動証明

3 “計算”に関する視点 19世紀末から20世紀初頭にかけて， 数学の世界における“計算という行為”に関する問題意識の萌芽
特にHilbert学派 数学基礎論の成立 自動機械(automaton)

4 ２種類の論証 演繹的推論 帰納的推論 他の命題から論理的に命題を導く “数学的帰納法”も含める 実験や観測に基づいて命題を導く
自然科学，社会科学など

5 演繹における命題，証明 命題：正しさを考察対象とする文 証明：命題から命題を次々と導く連鎖
数学では，その意義や用途に応じて，定理，補題，命題，公理，などと呼ばれる 証明：命題から命題を次々と導く連鎖

6 証明の例 考察の対象：ユークリッド幾何 定理 三角形ABCが二等辺ならば底角は等しい A B = A C ®ÐABC =Ð ACB A B

7 人手による“証明” 前提： AB=AC (1) (1)から AC=AB (2) 一方 ÐBAC º ÐCAB (3)
(1), (2), (3)に三角形の合同条件を適用して DBAC= DCAB (4) したがって ÐABC= ÐACB (5)

8 証明の構造 (1) AB=AC (3) ÐBAC º ÐCAB (2) AC=AB (1) AB=AC 合同条件
　 (4) DBAC = DCAB (5) ÐABC = ÐACB

9 明示的には用いていない命題 AB=AC (1) ® AC=AB (2) ÐBAC = ÐCAB (3) 三角形の合同条件
二辺とその挟角が等しい三角形は合同 DBAC º DCAB (4) ® ÐABC= ÐACB (5) 合同な三角形の角が等しい

10 公理 公理：証明なしで正しさを認める命題 証明の始点 例 前出の証明で用いる公理 等号の対称性: AB=AC ® AC=AB
　　証明の始点 証明：命題から命題を次々と導く連鎖Þ始点が必要 公理の設定が考察対象領域を決めてしまう． 例 前出の証明で用いる公理 等号の対称性: AB=AC ® AC=AB 角の対称性: ÐBAC=ÐCAB 合同: AB=EF AC=EG ÐBAC=ÐFEG ® DABC=DEFG 合同な三角形の角が等しい: DBAC º DCAB ® ÐABC= ÐACB

11 証明の構造 AB=AC AB=AC ® AC=AB ÐBAC º ÐCAB AC=AB AB=AC 合同条件
DBAC º DCAB ® ÐABC= ÐACB 　DBAC = DCAB 　ÐABC = ÐACB

12 証明の構造(2) AB=AC AB=AC ® AC=AB ÐBAC º ÐCAB AC=AB AB=AC
(ÐBAC º ÐCAB Ù AC=AB Ù AB=AC)® DBAC = DCAB DBAC º DCAB ® ÐABC= ÐACB 　DBAC = DCAB 　ÐABC = ÐACB

13 命題の構造と証明(1) AB=AC AB=AC ® AC=AB ÐBAC º ÐCAB AC=AB AB=AC
(ÐBAC º ÐCAB Ù AC=AB Ù AB=AC)® DBAC = DCAB DBAC º DCAB ® ÐABC= ÐACB 　DBAC = DCAB 　ÐABC = ÐACB

14 命題の構造と証明(2) ÐB=ÐC ÐB=ÐC ÐC=ÐB ÐC=ÐB ÐB=ÐC ÐC=ÐB ÐB=ÐC ÐC=ÐB ÐB=ÐC
BC=CB ÐC=ÐB ÐB=ÐC BC=CB Ù ÐC=ÐB Ù ÐB=ÐC Ù ÐC=ÐB Ù ÐB=ÐC BC=CB DBAC = DCAB DBAC = DCAB AB=AC DBAC = DCAB AB=AC

15 命題の構造と証明(3) 　　 　 ® Ù Ù ( Ù Ù )® ® 　 　 p p q r q p r q p r q p s s t s t

16 命題の構造と証明(4) 証明は命題中に用いられている論理結合子 ® (ならば) Ù (かつ) の用法に従って構成されている．
®　(ならば) 　　 Ù (かつ) の用法に従って構成されている． 用法と構成の関係は，命題が何を表しているかには依存しない． 表記法 j q d j q d j q d

17 推論規則(1) 推論規則：命題から命題を導くための規則 命題 j と j ®z から z を導く
命題中の論理結合子の用法で定まる 命題 j と j ®z　から z を導く “j と j ® z が成り立つので, z も成り立つ” j 　　　 j ® z 　　 z

18 推論規則(2) 命題 j と z から j Ù z を導く “j と z が成り立つので, j Ù z も成り立つ” j z j Ù z
命題 j1, j2 ,…, jn から j1Ùj2Ù…Ùjnを導く j1 j2 … jn j1Ùj2Ù…Ùjn

19 命題の構造と証明(3’) p p ® q r q p r Ù q Ù p (r Ù q Ù p) ® s s ® t s t 　

20 証明を構成する機械的手続き 証明したい論理式 z ® qと公理を表す論理式j1, j2 ,…, jnが与えられたとき, z , j1, j2 ,…, jn からq に至る証明を構成する手続き 例　 z ® q = p ® t, j1= p ® q, j2= r , j3= (r Ù qÙ p) ® s, j4= s ® t p p ® q r q p r Ù q Ù p (r Ù q Ù p) ® s s ® t s t

21 命題の構成方法 p p ® q r q p r Ù q Ù p (r Ù q Ù p) ® s s ® t s t 　

22 証明と探索(1) ある命題を証明するために適用可能な公理や命題は複数あり得る． 選択した公理や命題によっては証明が構成できないことがある．
s: DBAC = DCAB を結論とする命題は複数ある ÐB=ÐC Ù AC=AB Ù AB=AC ® DBAC = DCAB BC=CB Ù ÐC=ÐB Ù ÐB=ÐC ® DBAC = DCAB BC=CB Ù AC=AB Ù AB=AC ® DBAC = DCAB … 証明は全ての可能性を試すような“探索”によって見つける．

23 証明と探索(2) AND-OR木 p p p®q p®q r q p v u r v q p rÙqÙp vÙuÙr vÙqÙp
rÙqÙp®s vÙuÙr®s vÙqÙp®s s

24 一般性を持つ命題(1) これまでの証明で用いた公理は一般性をもつ 等号の対称性: AB=AC ® AC=AB
角の対称性: ÐBAC=ÐCAB 合同: (AB=EFÙAC=EGÙÐBAC=ÐFEG)® DABC=DEFG 合同な三角形の角が等しい: DBAC º DCAB ® ÐABC= ÐACB

25 一般性を持つ命題(2) これまでの証明で用いた公理は一般性をもつ 等号の対称性: x y= z u ® z u = x y
角の対称性: Ð x y z=Ð z y x 合同: (xy = uvÙ xz=uwÙÐyxz=Ðvuw)® Dxyz=Duvw 合同な三角形の角が等しい: Dyxz=Dvuw ® Ðxyz= Ðuvw

26 一般性を持つ命題(2) これまでの証明で用いた公理は一般性をもつ 等号の対称性: "x"y"z"u. xy=zu ® zu=xy
角の対称性: "x"y "z. Ð x y z=Ð z y x 合同: "x"y "z "u"v "w. (xy = uvÙ xz=uwÙÐyxz=Ðvuw)® Dxyz=Duvw 合同な三角形の角が等しい: "x"y"z"u"v"w.Dyxz=Dvuw®Ðxyz=Ðuvw

27 全称記号に対する推論規則 "x1"x2 …"xn. j j [x1 = t1, x2 = t2 ,…, xn = tn ]　　ti は具体的な対象 　例 "x"y"z"u. xy=zu ® zu=xy AB=AC ® AC=AB "x"y "z. Ð x y z=Ð z y x ÐBAC=ÐCAB

28 注意 命題の一般性の構造は，命題が表現する内容に依存する． 例 "x"y "z. Ð x y z=Ð z y x
"x"y. x z= z x 数理論理学では 命題論理: 一般性を扱わない 述語論理: 一般性を扱う

29 数学以外の領域への適用(1) p : Aは犯人である q : Aは現場にいた r : Aは別の場所にいた p ® q r ® Ø q
Ø q : q の否定 j Ø j ^ : 矛盾 ^

30 矛盾を導く証明(1) p p ® q r r ® Ø q q Ø q 　　　 ^

31 矛盾を導く証明(2) [p] p ® q r r ® Ø q q Ø q 　　　 ^ Ø p

32 数学以外の領域への適用(2) N M T K F S W 親子関係を表す記号を導入 x >f y ： x は y の父親
x >m y ： x は y の母親 x >p y ： x は y の親 x >gf y ： x は y の祖父 x >gm y ： x は y の祖母 male(x) ： x は男性 female(x) ： x は女性 N M T K F S W

33 親子関係の“公理” "x"y. x >p y Ù male(x) ® x >f y
"x"y. x >p y Ù female(x) ® x >m y "x"y"z. x >f y Ù y >p z ® x >gf z "x"y"z. x >m y Ù y >p z ® x >gm z N >p S F >p S S >p T M >p T male(N) female(F)

34 親子関係の“証明”の自動化 N >f y Ù y >pT ® N>gfT N>f y Ù y>pT

35 親子関係の“証明”の自動化 N>pS male(N)
N>pSÙmale(N)®N>f S N>pS Ù male(N) N>fS S>pT N>f SÙ S>pT ® N>gf T N>f S Ù S>pT N >gf T

36 証明と探索(3) AND-OR木 N>f y Ù y>pT N>f y Ù y>pT
N>p S male(N) N>p S Ù male(N) x >p y Ù male(x) ® x >f y N>f M M >pT N>f S S >pT N>f y Ù y>pT N>f y Ù y>pT x >f y Ù y >p z ® x >gf z N >gf T