Confluence of conditional rewrite systems

Nachum Dershowitz, Mitsuhiro Okada, G. Sivakumar

Research output: Chapter in Book/Report/Conference proceedingConference contribution

47 Citations (Scopus)


Conditional rewriting has been studied both from the point of view of algebraic data type specifications and as a computational paradigm combining logic and functional programming. An important issue, in either case, is determining whether a rewrite system has the Church-Rosser, or confluence, property. In this paper, we settle negatively the question whether “joinability of critical pairs” is, in general, sufficient for confluence of terminating conditional systems. We review known sufficient conditions for confluence, and also prove two new positive results for systems having critical pairs and arbitrarily big terms in conditions.

Original languageEnglish
Title of host publicationConditional Term Rewriting Systems - 1st International Workshop, Proceedings
EditorsStephane Kaplan, Jean-Pierre Jouannaud
PublisherSpringer Verlag
Number of pages14
ISBN (Print)9783540192428
Publication statusPublished - 1988
Externally publishedYes
Event1st International Workshop on Conditional Term Rewriting Systems, 1987 - Orsay, France
Duration: 1987 Jul 81987 Jul 10

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume308 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other1st International Workshop on Conditional Term Rewriting Systems, 1987

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Confluence of conditional rewrite systems'. Together they form a unique fingerprint.

Cite this