|
JAIST Repository >
School of Information Science >
Articles >
Journal Articles >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/10119/9067
|
| Title: | KBO Orientability |
| Authors: | Zankl, Harald
Hirokawa, Nao
Middeldorp, Aart |
| Keywords: | Knuth-Bendix order
term rewriting
termination |
| Issue Date: | 2009-08 |
| Publisher: | Springer |
| Magazine name: | Journal of Automated Reasoning |
| Volume: | 43 |
| Number: | 2 |
| Start page: | 173 |
| End page: | 201 |
| DOI: | 10.1007/s10817-009-9131-z |
| Abstract: | This article presents three new approaches to prove termination of rewritesystems with the Knuth-Bendix order efficiently. The constraints for theweight function and for the precedence are encoded inhbox{(pseudo-)}propositional logic or linear arithmetic and theresulting formula is tested for satisfiability using dedicated solvers.Any satisfying assignment represents a weight function and a precedencesuch that the induced Knuth-Bendix order orients the rules of the encodedrewrite system from left to right. This means that in contrast to thededicated methods our approach does not directly solve the problem buttransforms it to equivalent formulations for which sophisticatedback-ends exist.In order to make all approaches complete we present a method to computeupper bounds on the weights.Furthermore, our encodings take dependency pairs into accountto increase the applicability of the order. |
| Rights: | This is the author-created version of Springer, Harald Zankl, Nao Hirokawa, and Aart Middeldorp, Journal of Automated Reasoning, 43(2), 2009, 173-201. The original publication is available at www.springerlink.com, http://dx.doi.org/10.1007/s10817-009-9131-z |
| URI: | http://hdl.handle.net/10119/9067 |
| Material Type: | author |
| Appears in Collections: | b10-1. 雑誌掲載論文 (Journal Articles)
|
Files in This Item:
| File |
Description |
Size | Format |
|---|
| 13943-1.pdf | | 269Kb | Adobe PDF | View/Open |
|
All items in DSpace are protected by copyright, with all rights reserved.
|
