|
|||||
|
|
Deciding confluence of certain term rewriting systems in polynomial time |
|
| Authors: | Guillem Godoy Ashish Tiwari and Rakesh Verma |
| Institution: | a Technical University of Catalonia, Jordi Girona 1, Barcelona, Spain b SRI International, Menlo Park, CA, USA c Computer Science Department, University of Houston, TX, USA |
| Abstract: | We present a characterization of confluence for term rewriting systems, which is then refined for special classes of rewriting systems. The refined characterization is used to obtain a polynomial time algorithm for deciding the confluence of ground term rewrite systems. The same approach also shows the decidability of confluence for shallow and linear term rewriting systems. The decision procedure has a polynomial time complexity under the assumption that the maximum arity of a function symbol in the signature is a constant. |
| Keywords: | Term rewriting Confluence Ground rewrite systems Shallow linear rewrite systems |
| 本文献已被 ScienceDirect 等数据库收录！ | |