Characterizing and proving operational termination of deterministic conditional term rewriting systems

DOI10.1016/j.jlap.2009.08.001zbMath1206.68163OpenAlexW2150223040MaRDI QIDQ710679

Bernhard Gramlich, Felix Schernhammer

Publication date: 22 October 2010

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2009.08.001

zbMATH Keywords

conditional term rewritingoperational terminationcollapse extended terminationdependency pair frameworktransforming conditional rewrite systems

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Unnamed Item, Transformations of Conditional Rewrite Systems Revisited, Dependency pairs for proving termination properties of conditional term rewriting systems, An integrated framework for the diagnosis and correction of rule-based programs, Twenty years of rewriting logic, On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings, The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques, Completion after Program Inversion of Injective Functions, Applications and extensions of context-sensitive rewriting, Using well-founded relations for proving operational termination

Uses Software

• Maude
• AProVE
• MU-TERM
• CARIBOO
• VMTL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Mechanizing and improving dependency pairs
• Operational termination of conditional term rewriting systems
• ELAN from a rewriting logic point of view
• Termination of term rewriting using dependency pairs
• Proving operational termination of membership equational programs
• Transformation for Refining Unraveled Conditional Term Rewriting Systems
• Improving the Context-sensitive Dependency Graph
• Proving Termination of Context-Sensitive Rewriting with MU-TERM
• Unravelings and ultra-properties
• Transformations of Conditional Rewrite Systems Revisited
• Computationally Equivalent Elimination of Conditions
• Automated Termination Analysis for Logic Programs by Term Rewriting
• Local Termination
• From Outermost to Context-Sensitive Rewriting
• Operational Termination of Membership Equational Programs: the Order-Sorted Way
• Context-Sensitive Dependency Pairs
• Frontiers of Combining Systems
• Improving Context-Sensitive Dependency Pairs
• Term Rewriting and Applications
• Termination proofs of well-moded logic programs via conditional rewrite systems