2D Dependency Pairs for Proving Operational Termination of CTRSs

Autores UPV
Año
CONGRESO 2D Dependency Pairs for Proving Operational Termination of CTRSs

Abstract

The notion of operational termination captures nonterminating computations due to subsidiary processes that are necessary to issue a single `main' step but which often remain `hidden' when the main computation sequence is observed. This highlights two dimensions of nontermination: one for the infinite sequencing of computation steps, and the other that concerns the proof of some single steps. For conditional term rewriting systems (CTRSs), we introduce a new dependency pair framework which exploits such bidimensional nature of conditional rewriting (rewriting steps + satisfaction of the conditions as reachability problems) to obtain a powerful framework for proving operational termination of CTRSs.