Inductive thoeorems and ground confluence for conditional term rewriting systems

2021 Fiscal Year Final Research Report

• 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
• 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.

Free Research Field

項書き換え

Academic Significance and Societal Importance of the Research Achievements

項書き換えシステムは，論理的な推論体系と計算手続きを表わす計算体系と2面性を持つ計算モデルであり，合流性や帰納的な妥当性はその両方の側面を繋ぐ重要な性質と考えることができる．本研究は，安全なソフトウェアを構築するための基礎理論に関するものであり，長期的には情報システムの脆弱性の克服への貢献となるものと考えられる．