1998 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つのシステムの等価性判定法として、抽象リダクションシステムの枠組で考察し、書き換え帰納法と滞在帰納法の本質的な差は、強正規性と弱正規性、および退行性と合流性にもとづいていることを明らかにした。したがって、両者の証明能力は異なることが示された。
2. 反駁証明法と組み合せた場合の比較
滞在帰納法と書き換え帰納法に、それぞれ反駁証明法を組み合わせると、両者の証明能力が一致することを明らかにした。したがって、実際の自動証明システムでは両者の能力に実質的な差は生じない。
3. 自動証明システムとの対応
上記の抽象的な枠組みをもちいて、実際に作成されている自動証明システムのメカニズムの解析を試みた。いくつかのシステムの解析を通して、本研究の定式化は、実際のシステム解析手法として有効であることを確認した。
|
-
[Publications] M.Iwami: "An improved recursive decomposition ordering for higher-order rewriting systems" IEICE TRANS.INF.& SYST.E81-D-9. 988-996 (1998)
-
[Publications] M.Sakai: "Semantics and strong sequentiality of priority terns rewriting systems" Theoretical Comput.Sci.208. 87-110 (1998)
-
[Publications] T.Nagaya: "Index reduction of overlapping strongly sequential systems" IEICE TRANS.INF.& SYST.E81-D-5. 419-426 (1998)
-
[Publications] T.Aoto: "Termination transforonation by tree clifting ordering" Lectur Notes in Comput.Sci.1379. 256-270 (1998)
-
[Publications] 小池広高: "潜在帰納法と書き換え帰納法の比較" 信学技報. COMP-98-432. 65-72 (1998)
-
[Publications] M.Iwami: "Simplification ordering for higher-order rewrite systems" Trans.of IPS of Japan. (発表予定).
