(57)【要約】  【課題】無限木の探索において探索空間の膨張を抑えて効率のよい探索を行うことが可能な無限木探索方法、装置及び処理プログラム並びに該プログラムを記録した記録媒体の提供。  【解決手段】ノードの集合Ｖに属する各ノードを根とする探索木の部分木に対し、この各ノードより推論規則群を順次適用してこの部分木の非拡大枝を通って到達できるノードの全探索を行い推論問題の解を探索する閉包処理部２１と、この閉包処理部２１にて解が発見されなかったときに、探索木の探索済みのノードに対し適用可能かつ未適用の推論規則を適用することで、この探索木の拡大枝を所定数選択的に拡大し、この拡大によりノードに追加されたノードの集合を新たなノードの集合Ｖとし、このノードの集合Ｖを閉包処理部２１に通知する拡大処理部２２と、を具備させる特徴的構成手段の採用。  【選択図】図１
2006031523.tif 000002
【特許請求の範囲】
【請求項１】
初期条件群が設定された推論問題にそれぞれ所定の前提条件と帰結条件との組を有した推論規則群を適用することで探索木の深さが無限である無限木中から当該推論問題の解を探索するために、複数の前記推論規則群を蓄積した推論規則データベースを接続する無限木探索装置が実施する無限木探索方法であって、
前記推論問題の前記初期条件を入力された当該無限木探索装置が、当該推論問題に前記推論規則データベース中の前記推論規則群を適用して前記初期条件群に基づく前記探索木の根からなるノードの集合Ｖから所要の前記帰結条件を導くまで順次当該ノードの集合Ｖを更新しながら前記前提条件を対応させることで当該推論問題の解を探索するにあたり、
前記ノードの集合Ｖが入力された当該無限木探索装置が具備する閉包処理部が、当該ノードの集合Ｖに属する当該各ノードを根とする当該探索木の部分木に対し、前記推論規則データベース中の前記推論規則群を当該各ノードより順次適用して当該部分木の非拡大枝を通って到達できるノードの全探索を行い前記推論問題の解を探索する閉包過程と、
当該無限木探索装置が別途具備する拡大処理部が、当該閉包過程にて前記解が発見されなかったときに、前記閉包処理部から入力された当該探索木の探索済みの前記ノードに対し、前記推論規則データベース中の適用可能かつ未適用の前記推論規則を適用することで、当該探索木の拡大枝を所定数選択的に拡大し、当該拡大により当該ノードに追加されたノードの集合を新たなノードの集合Ｖとして当該閉包処理部に出力する拡大過程と、を前記閉包過程にて前記推論問題の解を発見するまで交互に繰り返すことで当該推論問題の解を探索する、
ことを特徴とする無限木探索方法。
【請求項２】
前記閉包過程は、
前記推論規則データベース中の所定の前記推論問題に対応させて事前に蓄積された推論規則群のうちの、前記探索木のノードに適用した場合に当該ノードの枝の拡大が有限に収まる非拡大枝に対応するよう事前に分類された非拡大枝推論規則群を読込み順次適用する一方、
前記拡大過程は、
当該推論規則群のうちの、前記探索木のノードに適用した場合に当該ノードの枝の拡大が無限となる拡大枝に対応するよう事前に分類された拡大枝推論規則を読込み適用する、
ことを特徴とする請求項１に記載の無限木探索方法。
【請求項３】
前記拡大過程は、
前記拡大により前記ノードに追加された前記新たなノード毎に対し直接的に適用可能となる前記推論規則の数を計数し、
その計数した当該数に基づき所定数の当該推論規則を幅優先で適用することで無限に拡大可能な前記拡大枝の中から前記所定数選択的な有限個の枝の拡大を為す、
ことを特徴とする請求項１又は２に記載の無限木探索方法。
【請求項４】
前記無限木探索方法は、
外部から前記推論問題の入力を受付け、
別途前記無限木探索装置に接続した定義情報データベース中の前記推論問題に対応した所定の定義情報群に基づき当該推論問題中の前記初期条件を認識し、
前記閉包過程において前記推論問題の解を発見した後に当該解を外部に出力する、
ことを特徴とする請求項１、２又は３に記載の無限木探索方法。
【請求項５】
前記推論問題の入力の受付けは、
それぞれ当該推論問題に対応した、前記定義情報データベースに登録すべく入力された所定の前記定義情報群と、前記推論規則データベースに登録すべく入力された前記推論規則群とのうちの１以上の入力を、当該推論問題の入力と併せて受付け、
引続き、それぞれ該当する当該定義情報データベース又は当該推論規則データベースに蓄積する、
ことを特徴とする請求項４に記載の無限木探索方法。
【請求項６】
初期条件群が設定された推論問題にそれぞれ所定の前提条件と帰結条件との組を有した推論規則を適用することで探索木の深さが無限である無限木中から当該推論問題の解を探索するために、複数の前記推論規則群を蓄積した推論規則データベースを接続した無限木探索装置であって、
当該無限木探索装置は、
前記推論問題に前記推論規則データベース中の前記推論規則を適用して前記初期条件群に基づく前記探索木の根からなるノードの集合Ｖから所要の前記帰結条件を導くまで順次当該ノードの集合Ｖを更新しながら前記前提条件を対応させることで当該推論問題の解を探索する推論規則適用部を具備して、
当該推論規則適用部は、
前記ノードの集合Ｖに属する当該各ノードを根とする当該探索木の部分木に対し、当該各ノードより前記推論規則群を順次適用して当該部分木の非拡大枝を通って到達できるノードの全探索を行い前記推論問題の解を探索する閉包処理部と、
当該閉包処理部にて前記解が発見されなかったときに、当該探索木の探索済みの前記ノードに対し適用可能かつ未適用の前記推論規則を適用することで、当該探索木の拡大枝を所定数選択的に拡大し、当該拡大により当該ノードに追加されたノードの集合を新たなノードの集合Ｖとし、当該ノードの集合Ｖを当該閉包処理部に通知する拡大処理部と、を具備して構成される、
ことを特徴とする無限木探索装置。
【請求項７】
前記推論規則データベースは、
前記推論規則群を所定の前記推論問題に対応させてそれぞれ、前記探索木のノードに適用した場合に当該ノードの枝の拡大が有限に収まる非拡大枝に対応するよう事前に分類された非拡大枝推論規則群と、
前記探索木のノードに適用した場合に当該ノードの枝の拡大が無限となる拡大枝に対応するよう事前に分類された拡大枝推論規則群と、を事前に蓄積して構成されて、
前記閉包処理部は、
前記推論規則データベース中の所定の前記非拡大枝推論規則群を読込み順次適用するよう機能構成される一方、
前記拡大処理部は、
前記推論規則データベース中の所定の前記拡大枝推論規則を読込み適用するよう機能構成される、
ことを特徴とする請求項６に記載の無限木探索装置。
【請求項８】
前記拡大処理部は、
前記拡大により前記ノードに追加された前記新たなノード毎に対し直接的に適用可能となる前記推論規則の数を計数し、その計数した当該数に基づき所定数の当該推論規則を幅優先で適用することで無限に拡大可能な前記拡大枝の中から前記所定数選択的な有限個の枝の拡大を為すよう機能構成される、
ことを特徴とする請求項６又は７に記載の無限木探索装置。
【請求項９】
前記無限木探索装置は、
前記推論規則適用部にて前記推論問題中の前記初期条件を認識可能に別途前記推論問題に対応した所定の定義情報を複数蓄積する定義情報データベースが接続されて、
外部から前記推論問題の入力を受付ける入力部と、
前記推論規則適用部にて発見した前記推論問題の解を外部に出力する出力部と、を具備して、
前記推論規則適用部は、
前記定義情報データベース中の前記定義情報を参照することで前記推論問題を認識可能に機能構成される、
ことを特徴とする請求項６、７又は８に記載の無限木探索装置。
【請求項１０】
前記入力部は、
それぞれ前記推論問題に対応した、前記定義情報データベースに登録すべく外部から入力された所定の前記定義情報群と、前記推論規則データベースに登録すべく外部から入力された前記推論規則群とのうちの１以上の入力を、当該推論問題の入力と併せて受付けて、それぞれ該当する当該定義情報データベース又は当該推論規則データベースに蓄積可能に機能構成される、
ことを特徴とする請求項９に記載の無限木探索装置。
【請求項１１】
コンピュータを請求項６に記載の前記無限木探索装置を構成する各手段として機能させるための無限木探索処理プログラム。
【請求項１２】
請求項１１に記載の前記無限木探索処理プログラムを記録したコンピュータ読み取り可能な無限木探索処理プログラムを記録した記録媒体。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、無限木探索方法、装置及び処理プログラム並びに該プログラムを記録した記録媒体に関し、詳しくは、複数の推論規則群を蓄積した推論規則データベースを接続する無限木探索装置において初期条件群が設定された推論問題にそれぞれ所定の前提条件と帰結条件との組を有した推論規則群を適用することで探索木の深さが無限である無限木中から当該推論問題の解を探索するための無限木探索方法、並びにその実施に直接使用される無限木探索装置、この無限木探索装置に導入して使用される無限木探索処理プログラム、該プログラムを記録した記録媒体に係わる。
【背景技術】
【０００２】
従来、推論問題の解を探索木から探索することで求める探索アルゴリズムとして、自分の子を全て探索してから子の子を全て探索していく幅優先探索や、深さを少しずつ増やしながら深さ優先で探索を行う反復深化法、幅を少しずつ広げながら深さ優先で探索を行う反復拡幅法等があり、例えば、反復深化法は以下に示す非特許文献１に、反復拡幅法は以下に示す非特許文献２に開示されている。
【０００３】
【非特許文献１】Richard E. Korf, Depth-First Iterative-Deepening: An Optimal Admissible Tree Search, Artificial Intelligence, Vol.27, pp.97-109, 1985.
【非特許文献２】Matthew L. Ginsberg and William D. Harvey, Iterative Braodening, Proceeding of the Eighth National Conference on Aritificial Intelligence, pp.216-220, 1990.
【０００４】
一方、推論問題の解を自動的に求める手法として、例えば、初等幾何の証明問題の推論を機械的に導くにあたり効果的に補助線を発見するメカニズムについて、本願発明者らは、以下に示す非特許文献３に開示した利用度による枝刈りを想到するに至っている。
【０００５】
【非特許文献３】宮本健司、関川浩、白柳潔、町田文彦, 「初等幾何における読みやすい証明の生成について」, 京都大学数理解析研究所講究録 1335, “Computer Algebra-Algorithms, Implementation and Application,”pp.20-27, 2003.
【発明の開示】
【発明が解決しようとする課題】
【０００６】
しかしながら、従来の幅優先探索では、解が深いところにある場合、その探索ステップは膨大なものとなり指数関数的な時間とメモリ領域の計算量を必要とするものであり、反復深化法では、分岐が多く解が深いところにある場合、解より浅い部分の無駄な探索が増加してしまい、さらに、反復拡幅法では、探索木が無限の場合、すぐに発散してしまうという問題があった。
【０００７】
ここにおいて、本発明の解決すべき主要な目的は、次のとおりである。
【０００８】
即ち、本発明の第１の目的は、無限木の探索において探索空間の膨張を抑えて効率のよい探索を行うことが可能な無限木探索方法、装置及び処理プログラム並びに該プログラムを記録した記録媒体を提供せんとするものである。
【０００９】
本発明の第２の目的は、探索木から最適解を探索するまでの無限方向の拡大枝を最小とすることが可能な無限木探索方法、装置及び処理プログラム並びに該プログラムを記録した記録媒体を提供せんとするものである。
【００１０】
本発明の第３の目的は、推論問題に固有の定義情報群又は推論規則群を推論問題とともに入力を受付けて登録可能な無限木探索方法、装置及び処理プログラム並びに該プログラムを記録した記録媒体を提供せんとするものである。
【００１１】
本発明の他の目的は、明細書、図面、特に、特許請求の範囲の各請求項の記載から、自ずと明らかになろう。
【課題を解決するための手段】
【００１２】
まず、本発明方法においては、ノードの集合Ｖが入力された当該無限木探索装置が具備する閉包処理部が、当該ノードの集合Ｖに属する当該各ノードを根とする当該探索木の部分木に対し、推論規則データベース中の推論規則群を当該各ノードより順次適用して当該部分木の非拡大枝を通って到達できるノードの全探索を行い推論問題の解を探索する閉包過程と、当該無限木探索装置が別途具備する拡大処理部が、当該閉包過程にて解が発見されなかったときに、閉包処理部から入力された当該探索木の探索済みのノードに対し、推論規則データベース中の適用可能かつ未適用の推論規則を適用することで、当該探索木の拡大枝を所定数選択的に拡大し、当該拡大により当該ノードに追加されたノードの集合を新たなノードの集合Ｖとして当該閉包処理部に出力する拡大過程と、を閉包過程にて推論問題の解を発見するまで交互に繰り返すことで当該推論問題の解を探索する、という特徴的構成手法を講じる。
【００１３】
また、本発明装置においては、無限木探索装置の推論規則適用部に、ノードの集合Ｖに属する当該各ノードを根とする探索木の部分木に対し、当該各ノードより推論規則群を順次適用して当該部分木の非拡大枝を通って到達できるノードの全探索を行い推論問題の解を探索する閉包処理部と、当該閉包処理部にて解が発見されなかったときに、当該探索木の探索済みのノードに対し適用可能かつ未適用の推論規則を適用することで、当該探索木の拡大枝を所定数選択的に拡大し、当該拡大により当該ノードに追加されたノードの集合を新たなノードの集合Ｖとし、当該ノードの集合Ｖを当該閉包処理部に通知する拡大処理部と、を具備して構成させる、という特徴的構成手段を講じる。
【００１４】
一方、本発明プログラムにおいては、コンピュータを本発明装置を構成する各手段として機能させる、という特徴的構成手順を講じる。
【００１５】
他方、本発明記録媒体においては、本発明プログラムを記録したコンピュータ読み取り可能としてなる、という特徴的構成手続を講じる。
【００１６】
さらに、具体的詳細に述べると、当該課題の解決では、本発明が次に列挙する上位概念から下位概念に亙る新規な特徴的構成手法、手段、手順又は手続を採用することにより、目的を達成するよう為される。
【００１７】
即ち、本発明方法の第１の特徴は、初期条件群が設定された推論問題にそれぞれ所定の前提条件と帰結条件との組を有した推論規則群を適用することで探索木の深さが無限である無限木中から当該推論問題の解を探索するために、複数の前記推論規則群を蓄積した推論規則データベースを接続する無限木探索装置が実施する無限木探索方法であって、前記推論問題の前記初期条件を入力された当該無限木探索装置が、当該推論問題に前記推論規則データベース中の前記推論規則群を適用して前記初期条件群に基づく前記探索木の根からなるノードの集合Ｖから所要の前記帰結条件を導くまで順次当該ノードの集合Ｖを更新しながら前記前提条件を対応させることで当該推論問題の解を探索するにあたり、前記ノードの集合Ｖが入力された当該無限木探索装置が具備する閉包処理部が、当該ノードの集合Ｖに属する当該各ノードを根とする当該探索木の部分木に対し、前記推論規則データベース中の前記推論規則群を当該各ノードより順次適用して当該部分木の非拡大枝を通って到達できるノードの全探索を行い前記推論問題の解を探索する閉包過程と、当該無限木探索装置が別途具備する拡大処理部が、当該閉包過程にて前記解が発見されなかったときに、前記閉包処理部から入力された当該探索木の探索済みの前記ノードに対し、前記推論規則データベース中の適用可能かつ未適用の前記推論規則を適用することで、当該探索木の拡大枝を所定数選択的に拡大し、当該拡大により当該ノードに追加されたノードの集合を新たなノードの集合Ｖとして当該閉包処理部に出力する拡大過程と、を前記閉包過程にて前記推論問題の解を発見するまで交互に繰り返すことで当該推論問題の解を探索してなる、無限木探索方法の構成採用にある。
【００１８】
本発明方法の第２の特徴は、上記本発明方法の第１の特徴における前記閉包過程を、前記推論規則データベース中の所定の前記推論問題に対応させて事前に蓄積された推論規則群のうちの、前記探索木のノードに適用した場合に当該ノードの枝の拡大が有限に収まる非拡大枝に対応するよう事前に分類された非拡大枝推論規則群を読込み順次適用する一方、前記拡大過程を、当該推論規則群のうちの、前記探索木のノードに適用した場合に当該ノードの枝の拡大が無限となる拡大枝に対応するよう事前に分類された拡大枝推論規則を読込み適用してなる、無限木探索方法の構成採用にある。
【００１９】
本発明方法の第３の特徴は、上記本発明方法の第１又は第２の特徴における前記拡大過程を、前記拡大により前記ノードに追加された前記新たなノード毎に対し直接的に適用可能となる前記推論規則の数を計数し、その計数した当該数に基づき所定数の当該推論規則を幅優先で適用することで無限に拡大可能な前記拡大枝の中から前記所定数選択的な有限個の枝の拡大を為してなる、無限木探索方法の構成採用にある。
【００２０】
本発明方法の第４の特徴は、上記本発明方法の第１、第２又は第３の特徴における前記無限木探索方法を、外部から前記推論問題の入力を受付け、別途前記無限木探索装置に接続した定義情報データベース中の前記推論問題に対応した所定の定義情報群に基づき当該推論問題中の前記初期条件を認識し、前記閉包過程において前記推論問題の解を発見した後に当該解を外部に出力してなる、無限木探索方法の構成採用にある。
【００２１】
本発明方法の第５の特徴は、上記本発明方法の第４の特徴における前記推論問題の入力の受付けを、それぞれ当該推論問題に対応した、前記定義情報データベースに登録すべく入力された所定の前記定義情報群と、前記推論規則データベースに登録すべく入力された前記推論規則群とのうちの１以上の入力を、当該推論問題の入力と併せて受付け、引続き、それぞれ該当する当該定義情報データベース又は当該推論規則データベースに蓄積してなる、無限木探索方法の構成採用にある。
【００２２】
また、本発明装置の第１の特徴は、初期条件群が設定された推論問題にそれぞれ所定の前提条件と帰結条件との組を有した推論規則を適用することで探索木の深さが無限である無限木中から当該推論問題の解を探索するために、複数の前記推論規則群を蓄積した推論規則データベースを接続した無限木探索装置であって、当該無限木探索装置が、前記推論問題に前記推論規則データベース中の前記推論規則を適用して前記初期条件群に基づく前記探索木の根からなるノードの集合Ｖから所要の前記帰結条件を導くまで順次当該ノードの集合Ｖを更新しながら前記前提条件を対応させることで当該推論問題の解を探索する推論規則適用部を具備して、当該推論規則適用部が、前記ノードの集合Ｖに属する当該各ノードを根とする当該探索木の部分木に対し、当該各ノードより前記推論規則群を順次適用して当該部分木の非拡大枝を通って到達できるノードの全探索を行い前記推論問題の解を探索する閉包処理部と、当該閉包処理部にて前記解が発見されなかったときに、当該探索木の探索済みの前記ノードに対し適用可能かつ未適用の前記推論規則を適用することで、当該探索木の拡大枝を所定数選択的に拡大し、当該拡大により当該ノードに追加されたノードの集合を新たなノードの集合Ｖとし、当該ノードの集合Ｖを当該閉包処理部に通知する拡大処理部と、を具備して構成されてなる、無限木探索装置の構成採用にある。
【００２３】
本発明装置の第２の特徴は、上記本発明装置の第１の特徴における前記推論規則データベースが、前記推論規則群を所定の前記推論問題に対応させてそれぞれ、前記探索木のノードに適用した場合に当該ノードの枝の拡大が有限に収まる非拡大枝に対応するよう事前に分類された非拡大枝推論規則群と、前記探索木のノードに適用した場合に当該ノードの枝の拡大が無限となる拡大枝に対応するよう事前に分類された拡大枝推論規則群と、を事前に蓄積して構成されて、前記閉包処理部が、前記推論規則データベース中の所定の前記非拡大枝推論規則群を読込み順次適用するよう機能構成される一方、前記拡大処理部が、前記推論規則データベース中の所定の前記拡大枝推論規則を読込み適用するよう機能構成されてなる、無限木探索装置の構成採用にある。
【００２４】
本発明装置の第３の特徴は、上記本発明装置の第１又は第２の特徴における前記拡大処理部が、前記拡大により前記ノードに追加された前記新たなノード毎に対し直接的に適用可能となる前記推論規則の数を計数し、その計数した当該数に基づき所定数の当該推論規則を幅優先で適用することで無限に拡大可能な前記拡大枝の中から前記所定数選択的な有限個の枝の拡大を為すよう機能構成されてなる、無限木探索装置の構成採用にある。
【００２５】
本発明装置の第４の特徴は、上記本発明装置の第１、第２又は第３の特徴における前記無限木探索装置が、前記推論規則適用部にて前記推論問題中の前記初期条件を認識可能に別途前記推論問題に対応した所定の定義情報を複数蓄積する定義情報データベースが接続されて、外部から前記推論問題の入力を受付ける入力部と、前記推論規則適用部にて発見した前記推論問題の解を外部に出力する出力部と、を具備して、前記推論規則適用部が、前記定義情報データベース中の前記定義情報を参照することで前記推論問題を認識可能に機能構成されてなる、無限木探索装置の構成採用にある。
【００２６】
本発明装置の第５の特徴は、上記本発明装置の第４の特徴における前記入力部が、それぞれ前記推論問題に対応した、前記定義情報データベースに登録すべく外部から入力された所定の前記定義情報群と、前記推論規則データベースに登録すべく外部から入力された前記推論規則群とのうちの１以上の入力を、当該推論問題の入力と併せて受付けて、それぞれ該当する当該定義情報データベース又は当該推論規則データベースに蓄積可能に機能構成されてなる、無限木探索装置の構成採用にある。
【００２７】
一方、本発明プログラムの第１の特徴は、コンピュータを上記本発明装置の第１の特徴に記載の前記無限木探索装置を構成する各手段として機能させるための無限木探索処理プログラムの構成採用にある。
【００２８】
他方、本発明記録媒体の第１の特徴は、上記本発明プログラムの第１の特徴に記載の無限木探索処理プログラムを記録したコンピュータ読み取り可能な無限木探索処理プログラムを記録した記録媒体の構成採用にある。
【発明の効果】
【００２９】
本発明によれば、探索木の深さが無限である無限木から推論問題の解を探索するにあたり、無限方向の探索を制限することで探索空間の膨張を抑えて、探索を網羅的にかつ効率よく行うことが出来る。また、閉包と拡大とで適用する推論規則群を非拡大枝と拡大枝とのそれぞれに適用するものであることを事前に分類してそれぞれ所定の推論規則を適用するようにしたときには、簡易な構成により迅速に推論規則群を適用することが可能となる。
【００３０】
加えて、拡大においてそのノードに追加された新たなノード毎に直接的に適用可能な推論規則の数を計数してこの数に基づき所定の推論規則を適用し、無限に拡大可能な拡大枝の中から有限個の枝のみの拡大を為すことで、無限方向の拡大枝の数を最小としてさらに効率的な探索を可能となる。しかも、この推論問題に基づく各条件を認識するための定義条件群を有し、外部から推論問題の入力を受付けその解を出力するようにした場合には、任意の推論問題に対応することが可能となる。
【００３１】
さらに、推論問題に対応した、例えば、この推論問題に固有である定義情報群又は推論規則群を推論問題とともに外部から入力を受付けて登録可能とした場合には、定義情報データベース及び推論規則データベースには種々の推論問題において共通に利用される最小の定義情報群又は推論規則群のみを事前に登録しておけばよく、データベース容量を小さくすることが可能となり、また、推論問題に固有等の新たな定義情報群や推論規則群が必須な場合においても推論問題毎に個別に対応することが出来る。
【発明を実施するための最良の形態】
【００３２】
以下、本発明の実施の形態につき、添付の図面を参照しつつ、装置例、方法例、プログラム例及び記録媒体例を順に挙げて説明する。
【００３３】
（装置例）
図１は、本発明装置の実施形態例である装置例の無限木探索装置αの機能構成図である。
【００３４】
同図に示すように、本装置例に係る無限木探索装置αは、初期条件群が設定された推論問題にそれぞれ所定の前提条件と帰結条件との組を有した推論規則を適用することでこの推論問題の解を探索木の深さが無限である無限木中から探索するために、複数の推論規則群を蓄積した推論規則データベース１を接続して構成されて、無限木探索装置αは、例えば、ＣＰＵ（Central Processing Unit）とメモリ等を搭載してコンピュータの基本的機能を有する。
【００３５】
この無限木探索装置αは、さらに、推論問題に推論規則データベース１中の推論規則を適用して初期条件群に基づく探索木の根からなるノードの集合Ｖから所要の帰結条件を導くまで順次このノードの集合Ｖを更新しながら前提条件を対応させていくことで、この推論問題の解を探索する推論規則適用部２を具備する。
【００３６】
これにより、無限木探索装置αの推論規則適用部２では、推論問題中の初期条件から解を探索する探索木の枝を推論規則データベース１中の推論規則群に基づき幾つかの種類に分類し、第１のグループに属する要素を必ずその枝が有限となるようにしておくことで有限方向の全探索を可能とし、第１のグループに属する要素のみの全探索と、引続き拡大処理部２２による第２のグループに属する要素に対して探索木の枝を拡大するようにしている。
【００３７】
また、第１のグループの探索が有限となる性質に関し、第１のグループをなす枝の種類の集合が包含関係について極大となるようにしてこの第１のグループを非拡大枝集合と呼び、その要素を非拡大枝、その補集合を拡大枝集合、その要素を拡大枝と呼んで説明する。さらに、非拡大枝集合の要素の全探索を閉包、拡大枝の集合の要素の探索を拡大と呼び、以下において、閉包と拡大とを交互に繰り返すことによって探索を行う手法を、ここでは、反復拡大法と呼んで説明する。
【００３８】
この拡大枝は、繰り返し探索を進めると有限には収まらない、つまり拡大枝とは無限方向に探索を進める効果を持つ枝であり、一方、非拡大枝は、探索空間を広げる効果を持たず、探索を有限方向に進める効果を持つ枝である。そのため、非拡大枝のみによる探索は有限方向であるから必ず飽和し、拡大枝の探索は無限方向であるから探索空間を拡大することになる。
【００３９】
そのため無限木探索装置αは、以上に説明した閉包と拡大とを行うために、推論規則適用部２に閉包処理部２１と拡大処理部２２とを具備して構成されて、閉包処理部２１は、ノードの集合Ｖに属する各ノードを根とする探索木の部分木に対し、この各ノードより推論規則群を順次適用してこの部分木の非拡大枝を通って到達できるノードの全探索を行い推論問題の解を探索するよう機能構成される。
【００４０】
一方、拡大処理部２２は、閉包処理部２１にて解が発見されなかったときに、探索木の探索済みのノードに対し適用可能かつ未適用の推論規則を、例えば、幅優先で適用することで、この探索木の拡大枝を所定数選択的に拡大し、この拡大によりノードに追加されたノードの集合を新たなノードの集合Ｖとし、このノードの集合Ｖを閉包処理部２１に通知するよう機能構成される。
【００４１】
したがって、無限木探索装置αによる無限木の探索では、探索空間を有限方向と無限方向とに分けて、閉包処理部２１の有限方向の全探索と拡大処理部２２の無限方向への空間の拡大とを交互に実行させることが可能となり、探索空間の膨張を抑えながら探索を行うことができる。
【００４２】
ここで、推論規則データベース１は、推論規則群を所定の推論問題に対応させてそれぞれ、探索木のノードに適用した場合にこのノードの枝の拡大が有限に収まる非拡大枝に対応するよう事前に分類された非拡大枝推論規則群と、探索木のノードに適用した場合にこのノードの枝の拡大が無限となる拡大枝に対応するよう事前に分類された拡大枝推論規則群と、を事前に蓄積してもよい。
【００４３】
このとき、閉包処理部２１は、推論規則データベース１中の所定の非拡大枝推論規則群を読込み順次適用するように機能構成される一方、拡大処理部２２は、推論規則データベース１中の所定の拡大枝推論規則を読込み適用するよう機能構成される。
【００４４】
また、拡大処理部２２は、拡大によりノードに追加された新たなノード毎に対し直接的に適用可能となる推論規則の数を計数し、その計数した数に基づき所定数の推論規則を幅優先で適用することで無限に拡大可能な拡大枝の中から所定数選択的な有限個の枝の拡大を為すよう機能構成されるとよく、これにより無限木探索装置αにて探索木を探索するにあたり、急速に拡大する拡大枝の膨張を適切に抑えて効率的な探索が可能となる。
【００４５】
さらに、無限木探索装置αは、推論規則適用部２にて推論問題中の初期条件を認識可能に別途推論問題に対応した所定の定義情報を複数蓄積する定義情報データベース３が接続されて、外部から推論問題の入力を受付ける入力部４と、推論規則適用部２にて発見した推論問題の解を外部に出力する出力部５と、を具備するとよく、このとき、推論規則群の前提条件と帰結条件との組は、それぞれ定義情報群を用いて構成されることとなる。
【００４６】
これにより、推論規則適用部２では、推論問題中の初期条件を定義情報データベース３中に蓄積された定義情報を参照することで認識可能となり、引続き、この推論問題に推論規則を適用しこの適用の際に得た帰結条件を認識可能となる。一方、入力部４では、定義情報データベース３中の定義情報により認識可能な任意の推論問題を受付けることが可能となる。
【００４７】
このとき、入力部４は、それぞれ推論問題に対応した、定義情報データベース３に登録すべく外部から入力された所定の定義情報群と、推論規則データベース１に登録すべく外部から入力された推論規則群とのうちの１以上の入力を、推論問題の入力と併せて受付けて、それぞれ該当する定義情報データベース３又は推論規則データベース１に蓄積可能に機能構成されると好適である。
【００４８】
（方法例）
次に、以上のように構成された無限木探索装置αにより実施される方法例を説明する。
図２は、本発明の方法例に係る無限木探索方法を説明するためのフロー図である。
【００４９】
同図に示すように、本方法例においては、無限木探索装置αにおいて、推論問題に推論規則データベース１中の推論規則群を適用して初期条件群に基づく探索木の根からなるノードの集合Ｖから所要の帰結条件を導くまで順次このノードの集合Ｖを更新しながら前提条件を対応させることで推論問題の解を探索するにあたり、閉包処理部２１による閉包過程（ＳＴ３）と拡大処理部２２による拡大過程（ＳＴ５）とをＳＴ３の閉包過程にて推論問題の解を発見するまで交互に繰り返す。
【００５０】
即ち、ＳＴ３の閉包過程においては、ノードの集合Ｖが入力された閉包処理部２１が、このノードの集合Ｖに属する各ノードを根とする探索木の部分木に対し、推論規則データベース１中の推論規則群をこの各ノードより順次適用してこの部分木の非拡大枝を通って到達できるノードの全探索を行い推論問題の解を探索する。
【００５１】
一方、ＳＴ３にて解を発見できなかったとき（ＳＴ４：Ｎｏ）には、ＳＴ５の拡大過程を実施し、拡大処理部２２が、閉包処理部２１から入力された探索木の探索済みのノードに対し、推論規則データベース１中の適用可能かつ未適用の推論規則を適用することで、この探索木の拡大枝を所定数選択的に拡大し、この拡大によりノードに追加されたノードの集合を新たなノードの集合Ｖとして閉包処理部２１に出力し、このノードの集合Ｖに対して再度ＳＴ３の閉包過程を行うようにする。
【００５２】
なお、推論規則データベース１の推論規則群が所定の推論問題に対応させてそれぞれ探索木のノードに適用した場合にこのノードの枝の拡大が有限に収まる非拡大枝に対応する非拡大枝推論規則と、探索木のノードに適用した場合にこのノードの枝の拡大が無限となる拡大枝に対応する拡大枝推論規則と、に事前に分類して蓄積されたときには、ＳＴ３の閉包過程では推論規則として非拡大枝推論規則を、ＳＴ５の拡大過程では推論規則として拡大枝推論規則を読込み適用するようにするとよい。
【００５３】
また、無限木探索装置αに定義情報データベース３と入力部４と出力部５とを具備させたときには、まず、入力部４にて外部から推論問題の入力を受付け（ＳＴ１）、定義情報データベース３中の推論問題に対応した所定の定義情報群に基づきこの推論問題中の初期条件を認識する（ＳＴ２）ようにして、その後ＳＴ３の閉包過程において推論問題の解を発見した後に（ＳＴ４：Ｙｅｓ）、この解を出力部５にて外部に出力して（ＳＴ６）終了するようにすることも可能である。
【００５４】
なお、ＳＴ１の推論問題の入力の受付けは、それぞれこの推論問題に対応した、定義情報データベース３に登録すべく入力された所定の定義情報群と、推論規則データベース１に登録すべく入力された推論規則群とのうちの１以上の入力を、推論問題の入力と併せて受付けて、それぞれ該当する定義情報データベース３又は推論規則データベース１に蓄積するようにしても構わない。
【００５５】
続いて、図３は、本方法例に係る拡大過程を説明するためのフロー図である。
【００５６】
同図に示すように、ＳＴ５に示した拡大過程では、このＳＴ５における拡大によりノードに追加された新たなノード毎に対し直接的に適用可能となる推論規則の数を計数し（ＳＴ５１）、その計数した数に基づき決定された推論規則の、例えば、１つ２つ等の所定数を幅優先で適用することで無限に拡大可能な拡大枝の中から所定数選択的な有限個の枝の拡大を為す（ＳＴ５２）ようにすることもできる。
【００５７】
（プログラム例及び記録媒体例）
引続き、以上に説明した方法例の実施に際し、コンピュータを無限木探索装置αを構成する各手段として機能させるための無限木探索処理プログラムの例と、当該無限木探索処理プログラムを記録したコンピュータ読み取り可能な記録媒体の例とを説明する。
【００５８】
以上の装置例及び方法例の説明から明らかなように、本発明における無限木探索装置αは、コンピュータの基本機能を具備しているため、本発明で実現しようとする所要の機能は、ソフトウェア・プログラム（探索アルゴリズム）により構成することができる。
【００５９】
即ち、所要の処理プログラムを構成するに際しては、無限木探索装置αに、推論問題に推論規則データベース１中の推論規則群を適用して初期条件群に基づく探索木の根からなるノードの集合Ｖから所要の帰結条件を導くまで順次このノードの集合Ｖを更新しながら前提条件を対応させることで推論問題の解を探索する処理手順を実行させるにあたり、（Ａ）ノードの集合Ｖに属する各ノードを根とする探索木の部分木に対し、この各ノードより推論規則群を順次適用してこの部分木の非拡大枝を通って到達できるノードの全探索を行い推論問題の解を探索する閉包処理手順と、（Ｂ）閉包処理手順にて解が発見されなかったときに、探索木の探索済みのノードに対し適用可能かつ未適用の推論規則を適用することで、この探索木の拡大枝を所定数選択的に拡大し、この拡大によりノードに追加されたノードの集合を新たなノードの集合Ｖとする拡大処理手順と、を閉包処理手順にて推論問題の解を発見するまで交互に繰り返し実行させるための記述を、当該処理プログラムに具備させる。
【００６０】
このとき、（Ａ）の閉包処理手順は、推論規則データベース１中の所定の推論問題に対応させて事前に蓄積された推論規則群のうちの、探索木のノードに適用した場合にこのノードの枝の拡大が有限に収まる非拡大枝に対応するよう事前に分類された非拡大枝推論規則群を読込み順次適用する処理手順を実行させる、一方、（Ｂ）の拡大処理手順は、推論規則群のうちの、探索木のノードに適用した場合にこのノードの枝の拡大が無限となる拡大枝に対応するよう事前に分類された拡大枝推論規則を読込み適用する処理手順を実行させるようにしてもよい。
【００６１】
また、（Ｂ）の拡大処理手順は、（Ｂ−１）拡大によりノードに追加された新たなノード毎に対し直接的に適用可能となる推論規則の数を計数する処理手順と、（Ｂ−２）その計数した数に基づき所定数の推論規則を幅優先で適用することで無限に拡大可能な拡大枝の中から所定数選択的な有限個の枝の拡大を為す処理手順と、を順次実行させるための記述を、当該プログラムに具備させるとよい。
【００６２】
さらに、無限木探索処理プログラムは、無限木探索装置αに、（Ｃ）外部から推論問題の入力を受付ける処理手順と、（Ｄ）定義情報データベース３中の推論問題に対応した所定の定義情報群に基づきこの推論問題中の初期条件を認識する処理手順と、（Ｅ）閉包処理手順において推論問題の解を発見した後に解を外部に出力する処理手順と、を順次実行させるための記述を、当該プログラムに具備させても構わない。
【００６３】
また、（Ｃ）の推論問題の入力を受付ける処理手順は、（Ｃ−１）それぞれこの推論問題に対応した、定義情報データベース３に登録すべく入力された所定の定義情報群と、推論規則データベース１に登録すべく入力された推論規則群とのうちの１以上の入力を、推論問題の入力と併せて受付ける処理手順と、（Ｃ−２）それぞれ該当する定義情報データベース３又は推論規則データベース１に蓄積する処理手順と、を順次実行させるための記述を、当該プログラムに具備させるとよい。
【００６４】
なお、上記無限木探索処理プログラムを記録した記録媒体を構成する場合には、任意の記録媒体に、当該無限木探索処理プログラムにおける（Ａ）〜（Ｅ）の各処理手順をコンピュータ読み取り可能に記録すればよい。
【実施例１】
【００６５】
続いて、本発明の実施の形態につき、添付の図面を参照しつつ、実施例１を説明する。なお、本実施例１では従来の幅優先探索による探索アルゴリズムとの比較を行いながら推論問題として初等幾何における証明問題を例に挙げて説明するものの、初等幾何の証明問題に限定されるものではない。
【００６６】
まず、初等幾何における証明問題を推論問題として入力を受付ける無限木探索装置αは、定義情報データベース３に、推論問題に対応した、ここでは、例えば、「Ｐは点である」、「線分ＡＢとＣＤの長さは等しい」、「点Ａ，Ｂ，Ｃ，Ｄは直線ｍ上にある」、「直線ｍと直線ｎとは平行」等の幾何学的条件を認識するための定義情報を複数事前に登録しておく。
【００６７】
これにより、推論規則適用部２は、定義情報データベース３中の定義情報を参照することで、推論問題中の初期条件、推論規則の前提条件と帰結条件とのそれぞれ所定の幾何学的条件を認識することが可能となり、このとき、定義情報は、例えば、適宜定義情報データベース３にアクセスすることで読み出すようにするとよい。
【００６８】
さらに、この幾何学的条件にここでは「世代」という概念を導入して説明する。まず、世代０は問題の仮定として与えられる初期条件のこととし、以下、世代ｎの幾何学的条件に推論規則データベース１中に登録された推論規則群を適用して得られた帰結条件を追加したものを世代ｎ＋１としている。
【００６９】
このとき、探索木との対応を述べると、例えば、枝が推論規則の適用であり、ノードは証明となり、また、世代は探索木の深さに対応することとなる。ここで、与えられた推論問題に補助点（補助線）を許す推論規則を適用した場合、いくらでも補助点を追加することが可能であることから、この推論問題の探索木の深さは無限となる。
【００７０】
図４は、推論規則例である補助点の追加について説明するための説明図であり、中点連結定理の適用を例として拡大処理部２２における拡大を補助点の追加を例に挙げて具体的に説明する。
【００７１】
同図（ａ）に示すように、三角形ＡＣＤにおいて、点ＢはＡＣの中点、点ＰはＡＤの中点である。このとき、ＢＰとＣＤが平行であり、かつ、ＢＰの長さはＣＤの長さの半分である、という帰結条件が得られるが、この推論により新たに追加される点は存在しない。
【００７２】
一方、同図（ｂ）に示すように、線分ＡＣ，ＣＤ及びＡＣの中点Ｂのみが与えられている。したがって、ＡＤの中点Ｐを取れば、ＢＰとＣＤが平行であり、かつ、ＢＰの長さはＣＤの長さの半分である、という帰結条件が得られる。この推論規則の適用では補助点Ｐが追加している。よって、推論規則を適用して新しく点が追加されない場合と、推論規則を適用することにより新しく点が追加される場合がある。
【００７３】
したがって、無限木探索装置αに、例えば、このような補助点（補助線）を許す推論規則を適用した反復拡大法を利用した場合には、探索木の枝は推論規則の適用であるから、各推論規則によって枝が分類可能であり、ここでは、補助点を追加する推論規則の適用が拡大枝となり、補助点を追加しない推論規則の適用が非拡大枝となる。
【００７４】
ここで、閉包処理部２１にてあるノードから順次、補助点の追加がない推論規則のみを適用していった場合、その部分木は有限である。なぜならば、補助点以外の幾何概念（直線、長さ、角度、交点）の数は点の数で抑えられるからである。
【００７５】
よって、例えば、初等幾何の証明問題を推論問題とした場合には、例えば、入力部４にて推論問題（仮定，ゴール）と推論規則群との入力を受付ける一方、出力部５にて仮定からゴールに至るまでの証明を出力するようにするとよく、この証明を得るために、無限木探索装置αは、入力部４に入力された仮定を認識して、以下、閉包処理部２１にて補助点を追加しない推論規則について、例えば、幅優先等の所定の全検索を行いゴールが見つかれば出力部５に証明を出力するようにして終了する閉包過程と、拡大処理部２２にて所定の位置に補助点を追加する拡大過程とを繰り返し実施するようにする。
【００７６】
なお、ここでは、推論規則データベース１に蓄積する推論規則として、例えば、
（１）中点連結定理（補助点の追加あり）
（２）中点連結定理（補助点の追加なし）
（３）二等辺三角形の性質１（二等辺三角形の両底角は等しい）
（４）二等辺三角形の性質２（両底角の等しい三角形は二等辺三角形）
（５）平行線の性質（同位角、錯角は等しい）
の５つの推論規則を登録しておくものとして説明し、このうち、例えば、推論規則（１）が拡大枝推論規則、他の推論規則（２），（３），（４），（５）が非拡大枝推論規則として説明する。
【００７７】
なお、ここでは、推論規則の例として、（１）の拡大枝推論規則と、（２）〜（５）の非拡大枝推論規則と、に事前に分類して蓄積されて、閉包処理部２１と拡大処理部２２とでそれぞれ事前に設定されたこの推論規則群を適用するものとして説明するものの、これに限定されるものではなく、例えば、推論規則適用部２において推論規則を適用するにあたり、推論規則データベース１中の推論規則群に対して拡大枝に対応するものであるか、非拡大枝に対応するものであるかを識別してそれぞれ閉包処理部２１又は拡大処理部２２にて適用するようにしても構わない。
【００７８】
次に、図５は本実施例１に係る推論問題とその解を説明するための説明図である。
【００７９】
同図（ａ）に示すように、無限木探索装置αにおいて、まず、入力部４にて、四角形ＡＢＣＤの二辺ＡＢとＣＤの長さは等しく、点ＥはＡＣの中点、点ＦはＢＤの中点であるものとして、直線ＢＡとＦＥが交わる点をＧ、直線ＢＡとＤＣが交わる点をＨ、直線ＦＥとＤＣが交わる点をＩとしたとき、∠ＨＧＩ＝∠ＥＩＣであることを証明せよという初期条件を有した推論問題の入力を受付ける。
【００８０】
このとき、出力部５では、推論規則適用部２における所定の閉包、拡大の繰り返しにより、同図（ｂ）に示すような、三角形ＣＡＢとＢＤＣに同時に中点連結定理（補助線追加）を適用しＢＣの中点Ｍを生成、中点連結定理よりＥＭの長さはＡＢの長さの１/２、ＦＭの長さはＤＢの長さの１/２となり、問題の前提条件により、ＡＢとＣＤの長さは等しいから、三角形ＥＭＦは二等辺三角形となり（ＥＭとＦＭが等しい長さの辺）、さらに中点連結定理のもう一つの帰結として、ＥＭとＡＢは平行、ＦＭとＤＣは平行となり、平行線の性質から、∠ＨＧＩ＝∠ＭＥＦ（同位角）、∠ＥＩＣ＝∠ＭＦＥ（錯角）となる。一方、二等辺三角形の二つの底角は等しいので、∠ＭＥＦ＝∠ＭＦＥであり、これにより、∠ＨＧＩ＝∠ＥＩＣが結論できる、という出力を行った。
【００８１】
この推論問題の解を出力するにあたり、従来の幅優先探索で求めさせた場合と、無限木探索装置αに反復拡大法を実施させて求めさせた場合に適用する推論規則の候補数と実際の適用数を以下の表１に示し、図６は、従来の幅優先探索による探索木と本実施例１における探索木の探索空間の比較を説明するための説明図であり、同図（ａ）は従来の幅優先探索の場合の探索木を、同図（ｂ）は本実施例１における反復拡大法の場合の探索木を示し、各々の三角形右下の数値はその探索領域の推論規則の適用（候補）数、カッコ内は追加した補助点の数を示す。
【００８２】
【表１】
2006031523.tif 000003
【００８３】
同図（ａ）と上記表１に示すように、従来の幅優先探索では、まず、世代１の幾何学的条件を得るために上記５つの推論規則を適用し、最初に与えられた初期条件に対して全部で１２の推論規則が適用可能であり、このとき、追加する補助点は１０個である。なお、同じ規則であっても、適用場所が異なるものは別に数えるものとした。
【００８４】
ここでは、新たに追加した幾何学的条件の中に証明の帰結は含まれないので、探索木を拡大して探索を進めると、推論規則の適用候補２２６個中の２２４番目を適用した帰結が証明したいものであることがわかる。
【００８５】
一方、同図（ｂ）に示すように、本実施例１の無限木探索装置αでは、まず、閉包処理部２１の世代０の閉包において、初期条件に基づく探索木の根からなるノードの集合Ｖに対して、補助点なしの推論規則で適用可能なものはなく（同図（ｂ）の左上の白い三角形と数値０が対応）、次いで、拡大処理部２２の拡大において、例えば、このノードの集合Ｖの各ノードに直接的に追加可能な、１つの（１）の補助点ありの中点連結定理を適用したノードの集合に属する各ノードに対して直接適用可能となる上記（２）〜（５）の推論規則の数を計数したときに、この数が最大であった２個の推論規則が適用可能な位置を認識して補助点を１つ追加することで、例えば、この探索木の１つの拡大枝を選択的に拡大し、このノードに追加されたノードの集合を新たに、例えば、世代１に属するノードの集合Ｖとした。
【００８６】
続いて、閉包処理部２１にてこの世代１に属するノードの集合Ｖの各ノードを根とする探索木の部分木に対し、この部分木の非拡大枝を通って到達できるノードについて所定の全探索を行う閉包を実施するものであるが、この非拡大枝に対する探索を、例えば、幅優先で行った場合には、その１世代目の推論規則の適用候補２３のうちの５つめの適用で解が発見された。
【００８７】
この世代で実際に推論規則を適用した探索領域は同図（ｂ）の影付で示した領域であり、無限木探索装置αに反復拡大法を実施することにより、補助点を追加する推論規則の適用の拡大を抑え、必要以上に探索空間を広げることなく証明（解）を発見することが可能である。
【実施例２】
【００８８】
次に、本発明の実施の形態につき、添付の図面を参照しつつ、従来の幅優先探索の探索アルゴリズムと比較して実施例２を説明する。なお、本実施例２では、初等幾何における上記実施例１とは異なる証明問題を推論問題とし、定義情報データベース３の定義情報群及び推論規則データベース１の推論規則群は上記実施例１と同様のものとして説明を省略する。
【００８９】
図７は、本実施例２に係る推論問題とその解を説明するための説明図である。
【００９０】
同図（ａ）に示すように、無限木探索装置αにおいて、まず、入力部４にて、四角形ＡＢＣＤの二辺ＡＢとＣＤの長さは等しいものとし、対角線ＡＣの中点をＭ、対角線ＢＤの中点をＮ、直線ＭＮとＡＢの交点をＥ、直線ＭＮとＣＤの交点をＦ、直線ＡＢとＣＤの交点をＧとしたとき、ＧＥ＝ＧＦであることを証明せよという初期条件を有した推論問題の入力を受付ける。
【００９１】
このとき、出力部５では、推論規則適用部２における所定の閉包、拡大の繰り返しにより、同図（ｂ）に示すような、ＢＣの中点Ｍを生成し、三角形ＣＡＢとＣＤＢに応じに中点連結定理を適用することで、ＭＰの長さはＡＢの長さの１/２、ＰＮの長さはＣＤの長さの１/２となり、推論問題の前提より、ＡＢとＣＤの長さは等しいから、三角形ＰＭＮは二等辺三角形となり（ＰＭとＰＮが等しい長さの辺）、二等辺三角形の二つの底角は等しいので、∠ＰＭＮ＝∠ＰＮＭが成り立ち、また、中点連結定理のもう一つの帰結として、ＭＰとＡＢは平行、ＰＮとＣＤは平行となり、平行線の性質から、∠ＧＥＦは二つの底角が等しく二等辺三角形となり、ＧＥ＝ＧＦが結論できる、という出力を行った。
【００９２】
この推論問題の解を出力するにあたり、従来の幅優先探索で求めさせた場合と、無限木探索装置αに反復拡大法を実施させて求めさせた場合に適用する推論規則の候補数と実際の適用数を以下の表２に示し、図８は、従来の幅優先探索による探索木と本実施例２における探索木の探索空間の比較を説明するための説明図であり、同図（ａ）は従来の幅優先探索の場合の探索木を、同図（ｂ）は本実施例２における反復拡大法の場合の探索木を示し、各々の三角形右下の数値はその探索領域の推論規則の適用（候補）数、カッコ内は追加した補助点の数を示す。
【００９３】
【表２】
2006031523.tif 000004
【００９４】
同図（ａ）と上記表２に示すように、従来の幅優先探索では、証明が得られるまでに追加した補助点の数は７５個、結論が得られた深さまでの探索木のノードの数は１７７１８個となり、実際に解が得られたのは、８４５番目のノードであった。
【００９５】
この幅優先探索の内訳は、推論問題の初期条件に対し１２個の推論規則が適用可能であり、補助点は６個追加したところで、求める解は得られないため、推論規則を適用して探索木を深化させると、推論規則が適用可能な規則は２５６個、補助点は６５個追加される。この世代でも求める解は得られないため、さらに推論規則の適用により探索木を深化させると、推論規則の適用候補の総数１７４５０個の規則のうち、５７７番目（補助点の追加は４個）で証明が得られた。
【００９６】
一方、同図（ｂ）に示すように、本実施例２の無限木探索装置αでは、追加した点の数は１個、探索木のノードの数は３１個となり、実際には、１０番目のノードで証明を得ることが出来た。
【００９７】
この反復拡大法の内訳は、入力を受付けた推論問題の初期条件に基づく世代０に属する探索木の根からなるノードの集合Ｖに対し、まず、閉包処理部２１の閉包において、補助点追加なしの推論規則で適用可能なものではなく（同図（ｂ）の左上の白い三角形と数値０が対応）、次いで、拡大処理部２２の拡大において、例えば、このノードの集合Ｖの各ノードに直接的に適用可能な上記（２）〜（５）の推論規則の数を計数したときに、その数が最大となる、ここでは２個の推論規則が同時に適用可能な位置を認識して補助点を１つ追加し、世代１となるよう探索木を拡大して、ノードの集合Ｖを更新する。
【００９８】
続いて、閉包処理部２１の閉包でこの世代１に属するノードの集合Ｖの各ノードを根とする探索木の部分木に対し、この部分木の非拡大枝を通って到達できるノードの全探探索を、例えば、幅優先で行い、その１世代目の推論規則の適用候補７個をすべて適用しても求める解は得られないので、引続き、拡大処理部２２で、適用可能かつ未適用、即ち、先の補助点とは異なる位置の導入可能な位置に補助点を導入して拡大枝を所定有限数に限定して拡大してノードの集合Ｖを更新した後、閉包処理部２１にて世代２のノードの集合Ｖに適用可能な適用候補２２個のうちの最初の枝で証明が得られた。
【００９９】
本実施例２の推論問題では、証明に必要な補助線を追加した後、２世代にわたって探索が必要となる場合について説明したが、この推論問題について幅優先探索により解を求めると、世代１で証明に必要な補助点が追加されているにもかかわらず、さらに世代２で多くの補助点を追加してしまい、その結果探索空間を大きく膨張させてしまっていた。それに対し、無限木探索装置αによる反復拡大法では、必要な補助線を追加した後の、無駄な探索を抑えることが可能となり、大幅な高速化につながる。
【０１００】
以上、本発明の実施の形態につき、その装置例、方法例、プログラム例及び記録媒体例並びに実施例１〜２を順次挙げて説明したが、本発明は、必ずしも上述した手法、手段、手順又は手続にのみ限定されるものではなく、前述した効果を有する範囲内において、適宜、変更実施することが可能なものである。
【図面の簡単な説明】
【０１０１】
【図１】本発明装置の実施形態例である装置例の無限木探索装置αの機能構成図である。
【図２】本発明の方法例に係る無限木探索方法を説明するためのフロー図である。
【図３】同上した拡大過程を説明するためのフロー図である。
【図４】推論規則例である補助点の追加について説明するための説明図である。
【図５】本実施例１に係る推論問題とその解を説明するための説明図である。
【図６】従来の幅優先探索による探索木と本実施例１における探索木の探索空間の比較を説明するための説明図である。
【図７】本実施例２に係る推論問題とその解を説明するための説明図である。
【図８】従来の幅優先探索による探索木と本実施例２における探索木の探索空間の比較を説明するための説明図である。
【符号の説明】
【０１０２】
α…無限木探索装置
１…推論規則データベース
２…推論規則適用部
２１…閉包処理部
２２…拡大処理部
３…定義情報データベース
４…入力部
５…出力部
【図１】
2006031523.tif 000005
【図２】
2006031523.tif 000006
【図３】
2006031523.tif 000007
【図４】
2006031523.tif 000008
【図５】
2006031523.tif 000009
【図６】
2006031523.tif 000010
【図７】
2006031523.tif 000011
【図８】
2006031523.tif 000012