数理論理学、論理プログラミング、自律エージェント
記号論理学、特にその一分野である論理プログラミングを研究分野としています。現在は、自律エージェントの記号論理による形式化、および論理プログラミングによる実現をテーマに研究を行っています。
記号論理学は、我々が行う推論の過程を記号化して捉えるものです。例えば、推論の際に用いる基本的な推論規則として、“p”と“pならばq”から“q”を導く「三段論法」があります。これは、“pならばq”を「p→q」と表すことにすると、2つの記号列「p」と「p→q」から「q」を導く操作と捉えることができます。
記号化することの利点の1つは、記号列に対する操作は計算機に行わせやすいという点です。実際、このようにして、 計算機に自動推論を行わせることができます。
また、“xのy乗はzである”を「exp(x,y,z)」と表し、2つの記号列
exp(x,0,1) …(A)
exp(x,y,z)→exp(x,y+1,x×z) …(B)
を計算機に与えておくと、計算機は(A)のxに3を代入したexp(3,0,1)と(B)から、上記の三段論法でexp(3,1,3)を導き、さらにそれと(B)から同様にexp(3,2,9)を導き…というように、3の累乗を次々計算できます。このように、計算の過程を推論で実現できるというのが「論理プログラミング」の基本的な考え方です。
現在の私は、論理プログラミングの考え方を用いて、周囲の状況を認識しながら、その時々に応じて推論を行い、自らの目標を設定して動作する、人間の代理エージェント(自律エージェント)のソフトウェア的実現に向けた研究を行っています。このためには、エージェント(あるいは人間)の心的状態(目標?信念など)、あるいはその時間的変化を記号で表現できるように、論理体系を拡張しておくと好都合です。
例えば“あることがら(pとする)の達成を目標とする”を「Goal(p)」と表し、“pが次の時刻(例えば1分後)に成り立つ”を 「Nexttime(p)」と表すことにすると、“次の時刻にpを達成することが目標ならば、今qを実行する”は 「Goal(Nexttime(p))→q」と表せます。
このように拡張すると、推論規則として三段論法だけでは不十分です。そこで、エージェントの心的状態やその時間変化、あるいは周囲からの不完全な情報などを的確に扱うため、様相論理や時相論理、矛盾許容論理などと呼ばれる拡張論理に基づいたエージェントの形式化や構築について、現在考えています。
また、機械的な推論だけでは、人間の代理をやらせるにはどうしても不十分な面が出てくるので、学習などの機構を使って補うことも考えています。
これらに関連して、学生の卒業研究などでは、上記の他、小型ロボットによる自律エージェントの行為決定、自律エージェントの感情表現、論理的思考による人狼プレーヤエージェント、なども扱っています。
その他
オープンソース?ソフトウェアとは、ソースコード(プログラミング言語で記述された、人間にとって可読なプログラム)を公開し、誰でも開発(拡張や不具合修正など)に参加できるようにしたソフトウェアのことで、広く使われているものがいろいろあります。私もそれらのソフトのいくつかに対する修正差分(パッチ)を出したり、自作のソフトのソースを公開して、そうした活動に微力ながら協力しています。そのうち自作のものは、研究室のFTPサイトで公開中です(下記参照)。