Dependency pairs for proving termination properties of conditional term rewriting systems

Salvador Lucas, José Meseguer

Research output: Contribution to journalArticle


The notion of operational termination provides a logic-based definition of termination of computational systems as the absence of infinite inferences in the computational logic describing the operational semantics of the system. For Conditional Term Rewriting Systems we show that operational termination is characterized as the conjunction of two termination properties. One of them is traditionally called termination and corresponds to the absence of infinite sequences of rewriting steps (a horizontal dimension). The other property, that we call V-termination, concerns the absence of infinitely many attempts to launch the subsidiary processes that are required to perform a single rewriting step (a vertical dimension). We introduce appropriate notions of dependency pairs to characterize termination, V-termination, and operational termination of Conditional Term Rewriting Systems. This can be used to obtain a powerful and more expressive framework for proving termination properties of Conditional Term Rewriting Systems.

Original languageEnglish (US)
Pages (from-to)236-268
Number of pages33
JournalJournal of Logical and Algebraic Methods in Programming
Issue number1
StatePublished - Jan 1 2017


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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Software
  • Logic
  • Computational Theory and Mathematics

Fingerprint Dive into the research topics of 'Dependency pairs for proving termination properties of conditional term rewriting systems'. Together they form a unique fingerprint.

  • Cite this