研究の背景
人工知能(AI)における重要なテーマの一つに、人間が行う常識的な推論や それを越える高次推論の自動化と高速化が挙げられている。 このような不完全な知識の計算機による処理を目指して、 論理をベースとした知識表現の理論研究が大きく発展したが、 高次推論の体系の効率的実現のための研究はあまりなされていない。
この点に関して、モデル生成型定理証明器MGTP上でさまざまな高次推論体系を 実現する手法がICOTの研究成果として提案されている。 特に、知識の追加により元の理論の定理が棄却されてしまう推論(非単調推論)や、 観測結果からその原因を説明するために仮説を生成する推論(アブダクション) に関する理論的基礎とMGTPによる計算手続きが研究されてきた。 MGTPは定理証明分野における高速なプルーバとしての役割以外に、 論理プログラミング分野において、選言付き論理プログラミング (disjunctive logic programming)のボトムアップ処理系としても 国際的に評価されている。後者におけるMGTPの側面ではとくに、 失敗による否定(negation as failure; NAF)の計算のための 「井上・越村・長谷川の方式」が、論理プログラムの安定モデル(stable model)の 代表的な計算方式の一つとして知られている。しかしながら、この方式および アブダクションのMGTPによる計算方式を実現したソフトウェアに関しては、 これまで未整備だったため、IFSとしては未だに登録されておらず、 国内外の数多くの研究者からの問合せに対して十分対応できていなかった。
このように、(1)高速なMGTPの整備が整いつつあり、(2)非単調推論とアブダクションを MGTPで計算させる理論がほぼ整い、(3)国際的にもプログラムの公開を希望する声が 多いことなどから、高次推論プログラムを整理してソフトウェアとして提供する 必要性は非常に大きいといえる。 さらに、アブダクションと非単調推論を同時に使う重要な応用としては、 ダイナミックに環境や知識が変化する問題領域において、 信念や状態の変化を伴う推論の実現が考えられる。 したがって、上記の高次推論に加えてこうした高度な知識表現をサポートする 言語を処理するプログラムもMGTP上で実現できるものと考えられる。
研究の目的
本研究においては、これまでのICOTでの理論的研究成果をさらに進め、 高次推論のより効率的な手続きを確立し、 高次推論の真の実用化に寄与することを目的とする。
これまでに得られている成果の拡張としては、アブダクションと非単調推論の 自然な統一を目指す。このために、アブダクティブ論理プログラミング (Abductive Logic Programming; 以下ALPと記す）の処理系をMGTP上に実現する。 ALPでは、非単調なデフォルトの否定であるNAFの記述に加えて、 アブダクションの機能も合わせ持っている、 論理プログラミングの拡張されたクラスである。 過去のALPの計算手続きの研究においては、 限定されたクラスに対するものしか存在していないが、 MGTPのボトムアップ計算の特徴を活かせば、 かなり広いクラスに対して健全かつ完全な手続きを得ることができる。 しかもこうしたALPの処理系を作ることで、NAFおよびアブダクションのMGTP上での 計算プログラムを同時に提供することができ、 国内外からの要望にも答えることができる。
また本研究では新たな技術として、状態変化が記述できる言語 (これをアクション言語と呼ぶ)の処理系をMGTP上に実現することも目指す。 状態変化を扱うことはAIにとって古典的な問題であるが、 最近ロボット・プランニングなどでも脚光を浴びている。 この問題では非単調推論やアブダクションの技術が有効である。 したがって上記ALP処理系の応用プログラムとして、あるいは さらなる発展系として、アクション言語処理系を位置付けている。