| Presentation | 2017-03-10 Proving Confluence of Hierarchical Conditional Term Rewriting Systems without Sufficient Completeness Takayuki Kuroda, Naoki Nishida, Hiroyuki Seki, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | A transformational approach to confluence proofs for conditional term rewriting systems (CTRS) has been investigated, but confluence of a CTRS defining sorting over natural numbers has not been proved yet by any existing confluence prover. Such a CTRS defines behavior of function symbols hierarchically, called a hierarchical CTRS, and is not sufficiently complete. In this article, we propose a method to prove confluence of hierarchical CTRSs that are not sufficiently complete. More precisely, we first extend rewriting induction for conditional equations to TRSs that are not sufficiently complete, and then we prove joinability of a conditional critical pair by inducing other conditions from the original conditional part. Next, we design a simplification order that takes conditional parts of rewrite rules into account, and propose a method to prove termination of hierarchical CTRSs by means of the designed simplification order. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | conditional term rewriting system / confluence / rewriting induction / sufficient completeness |
| Paper # | SS2016-77 |
| Date of Issue | 2017-03-02 (SS) |
| Conference Information | |
| Committee | SS |
|---|---|
| Conference Date | 2017/3/9(2days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | Kazuhiro Ogata(JAIST) |
| Vice Chair | Akio Nakata(Hiroshima City Univ.) |
| Secretary | Akio Nakata(Tokyo Inst. of Tech.) |
| Assistant | Kazuyuki Shima(Hiroshima City Univ.) |
| Paper Information | |
| Registration To | Technical Committee on Software Science |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Proving Confluence of Hierarchical Conditional Term Rewriting Systems without Sufficient Completeness |
| Sub Title (in English) | |
| Keyword(1) | conditional term rewriting system |
| Keyword(2) | confluence |
| Keyword(3) | rewriting induction |
| Keyword(4) | sufficient completeness |
| 1st Author's Name | Takayuki Kuroda |
| 1st Author's Affiliation | Nagoya University(Nagoya Univ.) |
| 2nd Author's Name | Naoki Nishida |
| 2nd Author's Affiliation | Nagoya University(Nagoya Univ.) |
| 3rd Author's Name | Hiroyuki Seki |
| 3rd Author's Affiliation | Nagoya University(Nagoya Univ.) |
| Date | 2017-03-10 |
| Paper # | SS2016-77 |
| Volume (vol) | vol.116 |
| Number (no) | SS-512 |
| Page | pp.pp.103-108(SS), |
| #Pages | 6 |
| Date of Issue | 2017-03-02 (SS) |