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

Salvador Lucas, Jose 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)
JournalJournal of Computer and System Sciences
Publication statusAccepted/In press - Jan 1 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

Cite this