Deciding confluence of certain term rewriting systems in polynomial time

, &
Annals of Pure and Applied Logic 130 (1-3):33-59 (2004)
  Copy   BIBTEX

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

Categories

Keywords

Reprint years

DOI

10.1016/j.apal.2004.04.005

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,783

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Termination and confluence in infinitary term rewriting.P. H. Rodenburg - 1998 - Journal of Symbolic Logic 63 (4):1286-1296.
Light affine lambda calculus and polynomial time strong normalization.Kazushige Terui - 2007 - Archive for Mathematical Logic 46 (3-4):253-280.
A term rewriting characterization of the functions computable in polynomial space.Isabel Oitavem - 2002 - Archive for Mathematical Logic 41 (1):35-47.
On polynomial time computation over unordered structures.Andreas Blass, Yuri Gurevich & Saharon Shelah - 2002 - Journal of Symbolic Logic 67 (3):1093-1125.
On Nondeterminism, Enumeration Reducibility and Polynomial Bounds.Kate Copestake - 1997 - Mathematical Logic Quarterly 43 (3):287-310.
Lecture notes on term rewriting and computational complexity.Harvey Friedman - manuscript
Machines Over the Reals and Non‐Uniformity.Felipe Cucker - 1997 - Mathematical Logic Quarterly 43 (2):143-157.
Term Rewriting Systems.Jürgen Giesl - 2004 - Bulletin of Symbolic Logic 10 (2):223-225.
Polynomial time operations in explicit mathematics.Thomas Strahm - 1997 - Journal of Symbolic Logic 62 (2):575-594.
Chapter 1: Term rewriting systems.J. W. Klop - 1992 - In S. Abramsky, D. Gabbay & T. Maibaurn (eds.), Handbook of Logic in Computer Science. Oxford University Press. pp. 1--116.
The Analytic Polynomial-Time Hierarchy.Herbert Baier & Klaus W. Wagner - 1998 - Mathematical Logic Quarterly 44 (4):529-544.
Cdiprover3: A tool for proving derivational complexities of term rewriting systems.Andreas Schnabl - 2010 - In T. Icard & R. Muskens (eds.), Interfaces: Explorations in Logic, Language and Computation. Springer Berlin. pp. 142--154.

Analytics

Added to PP
2014-01-16

Downloads
42 (#377,979)

6 months
14 (#178,038)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Add more citations

References found in this work

Add more references