1998 Fiscal Year Annual Research Report

二分決定グラフを用いたプログラム検証の自動化に関する研究

Research Project

Project/Area Number	09780231
Research Institution	Ibaraki University
Principal Investigator	近藤久茨城大学, 工学部, 助手 (40261739)
Keywords	二分決定グラフ / プログラム検証 / 停止性 / 項書換え系 / 完備化手続き
Research Abstract	今年度は、前年度に得られた結果を項書換え系完備化手続きに応用する研究を行なった。その概要は以下のようにまとめられる。 1. KnuthとBendixによって提案された完備化手続きは与えられた等式集合と等価で完備な項書換え系の生成を試みる(半)アルゴリズムである。等式集合を代数的仕様とすれば、完備化手続きは仕様から実行可能なプログラムを生成するコンパイラとみなすことができる。また、定理自動証明など種々の応用において非常に有用な手法でもある。しかし、完備化手続きの結果は与えられた簡約順序に大きく依存する。少なくとも以下の問題点が挙げられる。 (a) 生成される項書換え系の停止性を保証するための簡約順序を利用者に要求する。 (b) 簡約順序が不適当な場合、手続きが無限に継続する場合がある。 (c) 簡約順序が適当な場合にも(完備な項書換え系が存在するにもかかわらず)失敗する場合がある。研究代表者は(b)の問題点を解決するために、平成6、7年度の研究において複数の簡約順序を同時に扱う完備化手続きを提案、実現し、その成果を学術論文誌等に発表している。しかし、提案した手法では(a)の問題点が解決できていなかった。 2. 1(a)で述べた問題を解決するため、前年度提案した停止性検証のための二分決定グラフの利用法を平成6、7年度に研究した複数の簡約順序を同時に扱う完備化手続き対して適用し、新たな完備化推論規則を得た。 3. 2.で得た完備化推論規則を多くの項書換え系に適用し、その効果を確認した。 4. 現在も継続して、計算機上での実現及び改良を行っている。これまでの研究業績を国内全国大会、国際会議にて発表し、論文誌に投稿(採録決定)した。

Research Products
(6 results)

All Other

All Publications (6 results)

[Publications] 近藤久: "二分決定グラフを用いた項書換え系の停止性検証システム" 人工知能学会誌. 13・5. 154-166 (1998)
[Publications] 近藤久: "BDD表現を用いた複数優先順位を扱う項書換え系完備化推論規則" 第58回(平成11年前期)情報処理学会全国大会. 2. 241-242 (1999)
[Publications] M.Kurihara: "Completion for Multiple Reduction Orderings" J.of Automated Reasoning. (to appear).
[Publications] M.Kurihara: "Binary Decision Diagrams for Mechanical Verification of Precedence-based Termina-tion of Rewrite Rules" 5th.Pacific Rim International Conf.Artificial Intelligence(poster paper). 7-12 (1998)
[Publications] 近藤久: "二分決定グラフを用いた書換え型プログラムの停止性検証器" 情報処理学会研究報告. 97・112. 1-6 (1997)
[Publications] 尾形達哉: "二分決定グラフを用いた書換え型プログラムの停止性検証システム" 人工知能学会全国大会(第11回)論文集. 108-111 (1997)

1998 Fiscal Year Annual Research Report

二分決定グラフを用いたプログラム検証の自動化に関する研究

Principal Investigator

近藤 久 茨城大学, 工学部, 助手 (40261739)

Research Products

[Publications] 近藤 久: "二分決定グラフを用いた項書換え系の停止性検証システム" 人工知能学会誌. 13・5. 154-166 (1998)

[Publications] 近藤 久: "BDD表現を用いた複数優先順位を扱う項書換え系完備化推論規則" 第58回(平成11年前期)情報処理学会全国大会. 2. 241-242 (1999)

[Publications] M.Kurihara: "Completion for Multiple Reduction Orderings" J.of Automated Reasoning. (to appear).

[Publications] M.Kurihara: "Binary Decision Diagrams for Mechanical Verification of Precedence-based Termina-tion of Rewrite Rules" 5th.Pacific Rim International Conf.Artificial Intelligence(poster paper). 7-12 (1998)

[Publications] 近藤 久: "二分決定グラフを用いた書換え型プログラムの停止性検証器" 情報処理学会研究報告. 97・112. 1-6 (1997)

[Publications] 尾形 達哉: "二分決定グラフを用いた書換え型プログラムの停止性検証システム" 人工知能学会全国大会(第11回)論文集. 108-111 (1997)

近藤久茨城大学, 工学部, 助手 (40261739)

[Publications] 近藤久: "二分決定グラフを用いた項書換え系の停止性検証システム" 人工知能学会誌. 13・5. 154-166 (1998)

[Publications] 近藤久: "BDD表現を用いた複数優先順位を扱う項書換え系完備化推論規則" 第58回(平成11年前期)情報処理学会全国大会. 2. 241-242 (1999)

[Publications] 近藤久: "二分決定グラフを用いた書換え型プログラムの停止性検証器" 情報処理学会研究報告. 97・112. 1-6 (1997)

[Publications] 尾形達哉: "二分決定グラフを用いた書換え型プログラムの停止性検証システム" 人工知能学会全国大会(第11回)論文集. 108-111 (1997)