博士（工学）山本雅人 学位論文題名
部分例示手法に基づく定理自動証明に関する研究 学位論文内容の要旨
定理 自動 証 明は ，あ る論 理 式が 他の 論理 式か ら 論理 的に 帰結 でき る こと を示 すため に ，あ る論 理 式が 恒偽 であ る こと を示 すも ので あ る． その 応用 とし て ，質 問応 答シス テム，プ ログラムの分析や合成などめミある．一般に，任意の論理式に対して´區偽である こ とを 示す 手 続き は存 在し な いが ，実際に´直偽である論 理式に対しては，その論理式 が 恒偽 であ る こと を証 明す る 手続 きは 存在 する こ とが 知ら れて いる ． この よう な手続 き は完 全性 を もっ とぃ われ ， 定理 自動証明手続きがもつぺ き重要な性質のーつである．
定理 自動 証 明に 対す るこ れ まで の研 究は ，導 出 原理 と呼 ばれ る単 一 の推 論規 則に基 づ く方 法が 中 心で あっ た． 最 近に なっ て， 定理 証 明を 命題 論理 式の 充 足可 能性 問題を 繰 り返 し解 く こと に帰 着す る りダ クシ ョン 手法 が 注目 され ，そ のー つ に部 分例 示手法 が あ る ． 部 分 例 示 手 法 はJeroslowに よ っ て 提 案 され た もの で， 論理 式中 の 一部 の変 数 にHerbrand空 間 の 要 素 を 代 入 し た 論 理 式 を 次 々に 生 成し ，そ の充 足可 能 性を 繰り 返 し判 定し て 定理 証明 を行 う 手法 であ る，Jeroslowが 提案 した 方法 は ，関 数記 号を含 ま ない 論理 式 を対 象と して お り， 導出 原理 に基 づ く方 法に 比ぺ て， よ り小 さい クラス の 問題 にし か 適用 でき ない ． また ，節 形式 を前 提 とし てい ない ため に 計算 効率 が悪い などの欠 点があった・
本論 文で は ，関 数記 号を 含 む論 理式 に対 して 適 用可 能な 部分 例示 手 法に 基づ く新し い 定理 自動 証 明手 続き を構 築 し， その 完全 性を 証 明し てい る． さら に ，導 出原 理に基 づ く定 理自 動 証明 手続 きと の 比較 実験 を行 い， そ の有 効性 につ いて 検 討し てい る．そ の成果は ，以下のように要約できる ．
（1） Jcroslowの方 法と 比 較し て， より 大き な クラ スに 含ま れる 問 題に 適用 可能で ある．
(2)節 形 式 を 前 提 と し てい るた め， 命 題論 理の 充足 可 能性 を判 定す るた め の効 率の よいアル ゴリズムを用いることがで きる．
(3)導 出 原 理 に 基 づ く 方法 では 証明 が 困難 な問 題の 中 で， 提案 した 手続 き では 容易 に証明可 能な問題が存在することを 示している｜
本 論 文 は 全6章 で 構 成 さ れ て い る ． 各 章 の 概 要 は 以 下 の 通 り で あ る ． 第1章 は 序 論 で あ り ， 本 研 究 の 背 景 と そ の 目 的 に つ い て 述 べ て い る ． 第2章 で は ， 本 論 の 準 備と して 記号 論 理の 基礎 につ い て述 ぺて いる ．本 論 文で 提案 す る定 理自 動 証明 手続 きは ， 命題 論理 式の 充足 可 能性 問題 を繰 り返 し 解く こと により 定 理証 明を 行 うも ので ある ． この ため ，記 号論 理 にお ける もっ とも 基 本的 な体 系であ る 命題 論理 に 関し て， 特に ， 解釈 や充 足可 能性 に つい て説 明し てい る ．ま た， 第一階 述 語論 理の 基 礎と して ，任 意 の論 理式 が充 足可 能 性を 変え るこ とな し に節 集合 ヘ変換
が可能であることを示している．そして，節集合に対して充足可能性を判定するため の重要な定理である，Herbrandの定理などについて説明している．本論文で提案する 手続きや現在まで提案されているほとんどの 定理自動証明手続きは，このHerbrand の定理を基礎としている．
第3章では，定 理自動証明に対するこれまでの研究の中で，最も一般的な導出原理 に基づく方法を説明している．導出原理は2つの節から新たな節を生成するための推 論規則である．導出原理に基づく定理自動証明手続きは，この推論規則を節集合に対 して繰り返し適用し矛盾を意味する空節を導くことを目的とする反駁手続きである．
また，本論文ガ基礎としている部分例示手法の基本的概念について述べ，Jeroslowが 提案している方法について詳しく述ぺている．そして，Jeroslowの方法を用いて実際 にコンピュータによる定理証明を行う際の問題点について指摘し，本論文で提案する 手続きの目的を明確にしている．
第4章では，節 形式の論理式に対して適用可能な部分例示手法に基づく定理自動証 明手続きを考案し，その詳細について述べている．手続きは，(1)命題論理式の充足 可能性問題を解く，(2)純障害物と呼ばれる原子式の組を見っける，(3)その純障害物 を解消するために節集合に新たな節を加える，の3つの処理を繰り返すものである．
本章では，これらの処理の詳細についてそれぞれ例題を交えて述ぺている．さらに，
Jeroslowの方法との相違点などについて論じ，今回提案した手続きでは，Jeroslowの 方法では不可能であった関数記号を含む論理式を扱うことが可能となることを示して いる．また，提案した手続きの完全性を証明 している．
第5章では，提 案した手続きの効率化のため，命題論理式の充足可能性問題に関し て，(1)いかに高速に解くか，(2)どのような解が有効であるか，の検討を行なってい る．その際，導出原理に基づく定理自動証明 手続きとして有名なOTTERと の計算機 実験を行い，提案した手続きの特徴を明らか にしている．
第6章 で は ， 本 研 究 の 結 論 及 び 今 後 の 展 望 に つ い て 述 べ て い る ．
学位論文審査の要旨 主査 教
副査 教
授 大内 授 伊達
東 惇
副 査 教 授 和 田 充 雄 副査 助 教授 栗原正仁
学 位 論 文 題 名
部分例 示手法に 基づく 定理自動証明に関する研究
定理自動証明は，与えられた論理式が他の論理式から論理的に帰結できることを示すために，そ の論理式が恒偽であることを示すものである．その応用として，質問応答システム，プログラムの 分析や合成なと功ミある．定理自動証明に対するこれまでの研究は，導出原理に基づく方法が中心で あったが，定理証明を命題論理式の充足可能性問題を繰り返し解くことに帰着するりダクション手 法と して部分例示手法がJeroslowにより提案されている．し かしながら，1988年のJeroslowの 急逝 により部分例示手法に対する 研究は多くの重要な問題点 が未解決のまま中断されていた．
本 論文は，著者がJeroslowの研 究を継承して行った研究成果をまとめたものであり．その主要 な成果は，以下のように要約できる．
1．論理式が関数記号を含まない場合にしか適用できなかった部分例示手法に基づく定理自動証 明 手 続 き を ， 関 数 記 号 を 含 む 場 合 に も 適 用 可 能 と な る よ う に 拡 張 し て い る ． 2．提案した手続きの完全性を証明している，すなわち，提案した手続きは論理式が実際に恒偽 であるならばそれを有限ステップで証明することが可能である．
3．導出 原理に基づく方法との比較実 験を通して，提案した手続きの特徴や有効性を検証して いる．
本論文は全6章で構成されている．各章の概要は以下の通りである．
第1章 は 序 論 で あ り ， 本 研 究 の 背 景 と そ の 目 的 に つ い て 述 べ て い る ． 、 第2章では，本論の郎備として記母論理の基礎について述べている．記号論理における最も基本 的な体系である命題論理に関して，第一階述語論理について説明している．また．節集合に対して 充足・ciT能性を 判定するための重要な定理で あるHcrbraudの定理などについて説明している．
第3章では，定理自鋤証明に対するこれまでの研究の中で，最も一般的な導出原理に基づく方法 を説明している．また，本論文が基礎としている部分例示手法の基本的概念について述ベ，Jeroslow が提案している方法について詳しく述べている．そして，Jeroslowの方法を用いて実際にコンピュー タによる定理証明を行う際の問題点について指摘し，本論文で提案する手続きの目的を明確にして いる．
第4章では，節形式の論理式に対して適用可能な部分例示手法に基づく定理自動証明手続きを考 案し，その詳細に ついて述べている．手続きは，(1)命題論理式の充足可能性問題を解く，(2)純 障害物と呼ばれる原子式の組を見っける，(3)その純障害物を解消するために節集合に新たな節を
‑ 581ー
加え る，の3つの処理を繰り返すものである．本章では，これらの処理の詳細についてそれぞれ 例題を交えて述ぺている．さらに，Jeroslowの方法との相違点などについて論じ，今回提案した 手続きでは，Jeroslowの方法では不可能であった関数記号を含む論理式を扱うことが可能となる ことを示している．また，提案した手続きの完全性を証明している．
第5章では，提案した手続きの効率化のため，命題論理式の充足可能性問題に関して，(1）いか に高速に解くか，(2)どのような解が有効であるか，の検討を行なっている．その際，導出原理に 基づ く定理自動証明手続きとして有名なOTTERとの計算機実験を行い，提案した手続きの特徴を 明らかにしている．
第6章では，本研究の結論及び今後の展望について述べている．
これを要するに，著者は，部分例示手法に基づく定理自動証明手続きを構築し，その特徴を明ら かにすることで，定理自動証明に関する研究上有益な新知見を得ており，システム情報工学の進歩 に寄与すること大である：
よっ て 著 者 は， 北 海 道 大学 博 士 （ 工学 ） の 学 位を 授 与 さ れる 資 格 あ るも の と 認 める ．
一 ―582一
