エージェント指向言語FIage(5) : メタ知識を用いた自動証明

概要

論文の詳細を見る
実際の数学問題やプログラム生成/検証に自動証明を適用した場合、形式的論理体系のみに基づいたものでは、公理や補題などの知識の増大に対して、その探索空間が指数関数的に広がってしまい、組合せ論的爆発を招く場合が多い。この問題に対して、ヒューリスティックスや問題領域上の構造定理、類推をメタ知識として利用し、一種のプランニングを行うことによって探索空間を削減する研究が行われている。一方、プランニングの問題として、問題領域が大規模/複雑になった場合、プランニングの適用可能性チェックのコストや必要な知識(オペレータ)を事前にすべて与えることの困難性があげられる。これは自動証明のプランニングの場合にもあてはまる場合が多いと考えられる。この問題の解決策としては、マルチエージェントによるプランニング方式が提案されている。そこで我々は、両者の技術の特長を利用し、メタ知識/マルチエージェントによる自動証明の探索空間の削減と分散化を行なう試みを行っている。本稿では、構成的プログラミングに自動証明を応用したプログラム合成を類推/マルチエージェントによって実現する試みについて、概要を示す。また、こうした試みがエージェント指向言語Flageによって自然にモデル化できることを示す。
一般社団法人情報処理学会の論文
1993-09-27

エージェント指向言語FIage(5) : メタ知識を用いた自動証明

スポンサーリンク

概要

著者

関連論文

スポンサーリンク