Inductive thoeorems and ground confluence for conditional term rewriting systems
| Project/Area Number |
18K11158
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | Niigata University |
|---|
Principal Investigator |
Aoto Takahito 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| Project Period (FY) |
2018-04-01 – 2022-03-31
|
| Project Status |
Completed (Fiscal Year 2021)
|
| Budget Amount *help |
¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Fiscal Year 2020: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2019: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2018: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
|
|---|
| Keywords | 帰納的定理 / 基底合流性 / 条件付き項書き換えシステム / ホーン節論理 / 合流性 / 項書き換えシステム / ホーン節帰納的定理 / 補題生成法 / アンラベリング変換 / 定理自動証明 |
|---|
| Outline of Final Research Achievements |
Term rewriting is a model of computation based on equational logic. The notion of inductive theorems of term rewriting systems expresses validity of equations from the programming perspective, and conditional term rewriting systems are a rewriting framework that suits to model functional programs, based on horn-clause logic. In this project, we give a rewriting induction framework to prove horn-clause inductive theorems over conditional term rewriting systems. We also give a method to prove ground confluence of oriented conditional term rewriting systems, as well as a critical pairs criterion for level-commutativity of oriented conditional term rewriting systems, etc.
|
| Academic Significance and Societal Importance of the Research Achievements |
項書き換えシステムは，論理的な推論体系と計算手続きを表わす計算体系と2面性を持つ計算モデルであり，合流性や帰納的な妥当性はその両方の側面を繋ぐ重要な性質と考えることができる．本研究は，安全なソフトウェアを構築するための基礎理論に関するものであり，長期的には情報システムの脆弱性の克服への貢献となるものと考えられる．
|
Report
(5 results)
Research Products
(22 results)
-
-
-
[Journal Article] Commutative rational term rewriting2021
Author(s)
Mamoru Ishizuka, Takahito Aoto and Munehiro Iwami
-
Journal Title
Proceedings of the 15th International Conference on Language and Automata Theory and Applications (LATA 2021), Lecture Notes in Computer Science,
Volume: 12638
Pages: 200-212
DOI
ISBN
9783030681944, 9783030681951
Related Report
Peer Reviewed
-
-
-
-
-
-
-
-
-
-
-
-
[Journal Article] Confluence Competition 20182018
Author(s)
T. Aoto, M. Hamana, N. Hirokawa, A. Middeldorp J. Nagele, N. Nishida, K. Shintani, and Harald Zankl
-
Journal Title
Leibniz International Proceedings in Informatics (LIPIcs)
Volume: 108
DOI
NAID
Related Report
Peer Reviewed / Open Access / Int'l Joint Research
-
-
-
-
-
-
-
