研究の背景
人工知能(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処理系の応用プログラムとして、あるいはさらなる 発展系として、アクション言語処理系を位置付けている。