証明補完技法に基く仮説発見システムの構成

2001 Fiscal Year Annual Research Report

• Project/Area Number: 12680364
• Research Institution: Hokkaido University
• Principal Investigator: 山本 章博 北海道大学, 大学院・工学研究科, 助教授 (30230535)
• Keywords: 定理自動証明 / 証明補完 / 連結証明 / 仮説発見 / 残余仮説 / 帰納学習 / アブダクション / 適切さの論理

Research Abstract

既存の情報から新たな情報を得るためのシステムを,強固な理論的に裏付けに基いて開発することが本研究の目標である.
昨年度は,証明補完という独自に考案した論理的な推論を用いて仮説発見を論理的な行為として定式化し,連結証明法というHerbrandの定理を用いることにより,証明補完は残余仮説の構成として実現できることを明らかにし,従来,帰納推論や学習,アブダクションなど人工知能分野において個々ばらばらであった仮説発見の世界に,統一的な視点を与えることに成功した.
本年度の研究実績は,残余仮説の特性を分析し,それが適切さの論理(連関論理,relevant logic)によって特徴付けられることを明らかにした.適切さの論理は,ある知識から帰結された命題がその知識の一部を欠くともはや成立しない,というような帰結方法の定式化である.残余仮説は,背景知識と観測事実から適切さの論理によって構成される.このことは,仮説構成の手続きを定式化する際には,古典論理は必ずしも適切ではないことを示している.また,適切さの論理は部分構造論理の一種であることから,仮説の構成手法の能力を示す基準として,その構成手法を特徴付ける推論の構造がある,ということも示している.本年1月には,本研究と関連した研究者と情報交換するための場としてワークショップを北海道大学で開催した.
また,連結証明法の新たな実現方法について調査を行い,非常に単純化された実現方法が提案されていることが判明した.その方法は節を命題変数の列として扱うことが鍵となっている.この方法を残余仮説の構成に利用する方法について検討を開始した.この点は次年度も継続する予定である.

Research Products

• [Publications] Yamamoto, A, Fronfoefer, B: "Finding Hypotheses by Generalizing Residue Hypotheses"Proceedings of the Work in Progress session in the 11th International Workshop on Inductive Logic Programming. 107-116 (2001)