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

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

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

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

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

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

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

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

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

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

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

証明の構造(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

命題の構造と証明(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

命題の構造と証明(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

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

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

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

推論規則(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

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

証明を構成する機械的手続き 証明したい論理式 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

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

証明と探索(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 … 証明は全ての可能性を試すような“探索”によって見つける．

証明と探索(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

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

一般性を持つ命題(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

一般性を持つ命題(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

全称記号に対する推論規則 "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

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

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

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

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

数学以外の領域への適用(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

親子関係の“公理” "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)

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

親子関係の“証明”の自動化 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

証明と探索(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