(6) 制約 MGTP による知識表現と自然言語処理への応用

［中間報告］

１）研究進捗状況

本研究では、制約MGTPの適用領域を広げるために知識を制約として表現する方法について検討し、抽象度の高い知識表現言語処理系としての完成を目指す。そのために、現在、制約MGTPの制約機構を強化するための動的補題生成手法について、コネンションタブロー上で開発された手法を中心に洗い出し調査検討を重ねている。これらの手法を制約MGTP上へ形式的に移し変えるとともに、並列実装のための手法についてもいくつかの方法を検討中である。その1つについてはKLICによる実装に着手したところである。

２）現在までの主な成果

できるだけ短い証明を狭い探索領域で得るために、コネクションタブロー法で開発された種々の改良法を調査した。中でも後向きカット規則を組み込むことで短い証明木を作り出す方法に着目した。この後向きカット規則の制御法には、folding-down と folding-up の2つの手法があり、folding-up はコネクションタブロー計算で補題を生成し統合するための効率的な方法である。また、folding-down はコネクション計算やモデル消去法で使うfactorization 規則の一形態とみなせる。
これらの手法はコネクションタブロー法の逐次実行環境を想定している。我々はこの手法の中で、まずは folding-down を制約MGTP上での推論規則に移し変え、形式的に整理しなおした。また、並列実行のために必要な整合性のチェックなども付加した上で、folding-donw を用いた動的補題生成の実装法を整理した。

３）今後の研究概要

今年度は、調査検討した内容に従って folding-down の制約MGTP上への並列実装を進める。なお、もう1つの動的補題生成手法であるfolding-up は、トップダウンに計算をしながらボトムアップに補題生成をする方法であり分散環境での並列実装については困難が予想されるが引続き実装法を検討し folding-down とともに制約MGTPに組み込むための手法について提案をおこなう予定である。

４）今年度目標成果（イメージ）

従来の逐次のコネクションタブロー法で開発された補題生成法に関する手法を制約MGTPに移し変えて形式的に整理する。また、制約MGTP上での並列実装のための手法を提案し実装を行う。その上で従来のMGTPと比較実験を行い、証明長においてより短い証明が得られることから我々の手法の優位性を示す。