1999 Fiscal Year Annual Research Report
| Project/Area Number |
10680346
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
外山 芳人 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (00251968)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
鈴木 大郎 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (90272179)
|
|---|
| Keywords | 項書き換えシステム / 自動証明 / 潜在帰納法 / 書き換え帰納法 |
|---|
| Research Abstract |
項書き換えシステムに基づく帰納的定理の自動証明手法として提案されている潜在帰納法と書き換え帰納法の差異を解析するとともに、自動証明に有効な関連手法を研究し、以下の成果を得た。
1.書き換え帰納法の解析
潜在帰納法と書き換え帰納にそれぞれ反駁証明法を組み合わせると、両者の証明能力は理論的に一致することを明らかにするとともに、実際の証明システム上では両者の証明能力に差異が生ずる原因を解析した。その結果、前者はシステム全体の合流性を検証する必要があるため証明手続きが横型探索にもとづいているが、一方、後者は証明すべき対象のみに対する退行性の検証のみが必要とされるので証明手続きは縦型探索にもとづいており、それが実際の証明システム上での差異の生じた原因であることを明らかにした。
2.停止条件の解析
書き換えシステムにもとづく自動証明システムでは,リダクションの停止性を自動的に判定する手法の確立が重要である。依存対を拡張して、従来よりも強力な判定手法を確立した。
|
-
[Publications] 小池 広高: "潜在帰納法と書き換え帰納法の比較"コンピュータソフトウェア. (発表予定).
-
[Publications] K.Kusakari: "Argument filtering transformation"Lecture Notes in Comp.Sci.. 1702. 47-61 (1999)
-
[Publications] 中村正樹: "消去法による項書き換え系の停止性判定について"信学会論文誌. J82-D-1. 1225-1231 (1999)
-
[Publications] T.Nagaya: "Decidability for left-linear growing term rewriting systems"Lecture Notes in Comp.Sci.. 1631. 256-270 (1999)
-
[Publications] M.Iwami: "Simplification ordering for higher-order rewrite systems"Inf.Pro.Soci.of Japan Trans.on Programming. 40. 1-10 (1999)
-
[Publications] K.Kusakari: "On proving AC-termination by argument filtering method"Inf.Pro.Soci.of Japan Trans.on Programming. (発表予定).
