二分決定グラフを利用した完備化手続きの自動化とその統合環境構築に関する研究

2000 年度 実績報告書

• 研究課題/領域番号: 11780184
• 研究機関: 茨城大学
• 研究代表者: 近藤 久 茨城大学, 工学部, 助手 (40261739)
• キーワード: 二分決定グラフ / プログラム検証 / 停止性 / 項書換え系 / 完備化手続き / 遺伝的プログラミング

研究概要

今年度は前年度に行なった研究をもとに二分決定グラフを利用した完備化手続きの実現とその統合環境構築に関する研究を行なった。その概要は以下のようにまとめられる。
1.簡約順序として関数記号の集合上の(厳格)半順序(優先順位)に基づく経路順序を用いて、ある条件を満たす優先順位を自動的に(複数)生成する完備化推論規則を考案した。
2.1.で得られた結果をもとに完備化手続きの実現をおこなった。
3.統合環境構築の実現を現在も遂行中である。
平成11年度に考案した推論規則を元に実現した完備化手続きを用いて、現在も多くの実験を行なっている。小規模な問題に対しては、自動的に半順序(優先順位)を生成することが可能であるが、大規模な問題に対しては、効率的な問題が生じる。今後の課題として、大規模問題に如何にして対応するかが残されている。派生した研究として、遺伝的プログラミング(GP)による項書換え系の自動合成というテーマにも取り組んでいる。GPは遺伝的操作によって木構造で表されるプログラムの合成を行なう手法である。現在までの研究で基本的なリスト操作関数を合成することに成功しており、今後、適合度関数、遺伝的操作の工夫などを検討し、大規模な項書換え系の合成に適用する予定である。これらの成果を、国内所属学会全国大会、国際会議等で発表した。

研究成果

• [文献書誌] M.Kurihara: "Completion for Multiple Reduction orderings"J.of Automated Reasoning. 23. 25-42 (1999)
• [文献書誌] H.Kondo: "Design and Heuristics for BDD-based Automated Termination Verification System for Rule-based Programs"Proc.of 1999 IEEE International Conf. on Systems, Man and Cybernetics. V. 738-743 (1999)
• [文献書誌] M.Kurihara: "Heuristics and Experiments on BDD Representation of Boolean Functions for Expert Systems in Software Verification Domains"Proc.of 12th Australian Joint Conf.on Artificial Intelligence,AI'99. 353-364 (1999)
• [文献書誌] 近藤久: "BDD表現を用いた複数優先順位を扱う項書換え系完備化推論規則"第58回(平成11年前期)情報処理学会全国大会. 2. 241-242 (1999)
• [文献書誌] M.Kurihara: "BDD Encoding for Partial Order Constraints and Its Application to Software Verification"Proc.of 2000 IEEE International Conf. on Systems,Man and Cybernetics. 2062-2067 (2000)
• [文献書誌] 近藤久: "遺伝的プログラミングを用いた項書換え系の合成"第62回(平成13年前期)情報処理学会全国大会. 2. (2001)