| IEICE Technical Committee Submission System Conference Paper's Information |
Online Proceedings [Sign in] Tech. Rep. Archives |
| Go Top Page | Go Previous | [Japanese] / [English] |
| Paper Abstract and Keywords | ||
| Presentation | 2008-05-29 13:30 On Rewriting Induction for Presburger-Constrained Term Rewriting Systems Tsubasa Sakata, Naoki Nishida, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari (Nagoya Univ.)  SS2008-1 KBSE2008-1 |
|
| Abstract | (in Japanese) | (See Japanese page) |
| (in English) | A method for verifying equivalence between procedural programs has been proposed, where the implicit induction is extended to deal with constrained term rewriting systems. However, the rewriting induction, which is used for proving inductive theorems, has not been adapted to constrained systems yet. In this paper, we extend the rewriting induction for constrained term rewriting systems, and propose a procedure based on the method for proving constrained inductive theorems. In the case that constraints are Presburger formulas, we show an example of inductive theorems of which the proof by the procedure is simpler than by the method based on implicit induction. |
|
| Keyword | (in Japanese) | (See Japanese page) |
| (in English) | constrained TRS / rewriting induction / program verification / / / / / | |
| Reference Info. | IEICE Tech. Rep., vol. 108, no. 64, SS2008-1, pp. 1-6, May 2008. | |
| Paper # | SS2008-1 | |
| Date of Issue | 2008-05-22 (SS, KBSE) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| Copyright and reproduction |
All rights are reserved and no part of this publication may be reproduced or transmitted in any form or by any means, electronic or mechanical, including photocopy, recording, or any information storage and retrieval system, without permission in writing from the publisher. Notwithstanding, instructors are permitted to photocopy isolated articles for noncommercial classroom use without fee. (License No.: 10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| Download PDF | SS2008-1 KBSE2008-1 |
|
| Conference Information | |
| Committee | KBSE SS |
| Conference Date | 2008-05-29 - 2008-05-30 |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | Miyazaki Citizens' Plaza |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | general |
| Paper Information | |
| Registration To | SS |
| Conference Code | 2008-05-KBSE-SS |
| Language | Japanese |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | On Rewriting Induction for Presburger-Constrained Term Rewriting Systems |
| Sub Title (in English) | |
| Keyword(1) | constrained TRS |
| Keyword(2) | rewriting induction |
| Keyword(3) | program verification |
| Keyword(4) | |
| Keyword(5) | |
| Keyword(6) | |
| Keyword(7) | |
| Keyword(8) | |
| 1st Author's Name | Tsubasa Sakata |
| 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 | Toshiki Sakabe |
| 3rd Author's Affiliation | Nagoya University (Nagoya Univ.) |
| 4th Author's Name | Masahiko Sakai |
| 4th Author's Affiliation | Nagoya University (Nagoya Univ.) |
| 5th Author's Name | Keiichirou Kusakari |
| 5th Author's Affiliation | Nagoya University (Nagoya Univ.) |
| 6th Author's Name | |
| 6th Author's Affiliation | () |
| 7th Author's Name | |
| 7th Author's Affiliation | () |
| 8th Author's Name | |
| 8th Author's Affiliation | () |
| 9th Author's Name | |
| 9th Author's Affiliation | () |
| 10th Author's Name | |
| 10th Author's Affiliation | () |
| 11th Author's Name | |
| 11th Author's Affiliation | () |
| 12th Author's Name | |
| 12th Author's Affiliation | () |
| 13th Author's Name | |
| 13th Author's Affiliation | () |
| 14th Author's Name | |
| 14th Author's Affiliation | () |
| 15th Author's Name | |
| 15th Author's Affiliation | () |
| 16th Author's Name | |
| 16th Author's Affiliation | () |
| 17th Author's Name | |
| 17th Author's Affiliation | () |
| 18th Author's Name | |
| 18th Author's Affiliation | () |
| Speaker | Author-1 |
| Date Time | 2008-05-29 13:30:00 |
| Presentation Time | 30 minutes |
| Registration for | SS |
| Paper # | SS2008-1, KBSE2008-1 |
| Volume (vol) | vol.108 |
| Number (no) | no.64(SS), no.65(KBSE) |
| Page | pp.1-6 |
| #Pages | 6 |
| Date of Issue | 2008-05-22 (SS, KBSE) |
[Return to Top Page]