The 2D Dependency Pair Framework for conditional rewrite systems. Part I: Definition and basic processors

Salvador Lucas, José Meseguer, Raúl Gutiérrez

Research output: Contribution to journalArticle


Different termination properties of conditional term rewriting systems have been recently described emphasizing the bidimensional nature of the termination behavior of conditional rewriting. The absence of infinite sequences of rewriting steps (termination in the usual sense), provides the horizontal dimension. The absence of infinitely many attempts to launch the subsidiary processes that are required to check the rule's condition and perform a single rewriting step has been called V-termination and provides the vertical dimension. We have characterized these properties by means of appropriate notions of dependency pairs and dependency chains. In this paper we introduce a 2D Dependency Pair Framework for automatically proving and disproving all these termination properties. Our implementation of the framework as part of the termination tool MU-TERM and the benchmarks obtained so far suggest that the 2D Dependency Pair Framework is currently the most powerful technique for proving operational termination of conditional term rewriting systems.

Original languageEnglish (US)
Pages (from-to)74-106
Number of pages33
JournalJournal of Computer and System Sciences
StatePublished - Sep 2018


  • Conditional term rewriting
  • Dependency pairs
  • Operational termination
  • Program analysis

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Networks and Communications
  • Computational Theory and Mathematics
  • Applied Mathematics

Fingerprint Dive into the research topics of 'The 2D Dependency Pair Framework for conditional rewrite systems. Part I: Definition and basic processors'. Together they form a unique fingerprint.

  • Cite this