The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors

DOI10.1016/j.jcss.2018.04.002zbMath1393.68088OpenAlexW2800121675MaRDI QIDQ1635507

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

Publication date: 6 June 2018

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jcss.2018.04.002

zbMATH Keywords

program analysisconditional term rewritingdependency pairsoperational termination

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Automatically Proving and Disproving Feasibility Conditions, mu-term: Verify Termination Properties Automatically (System Description), Local confluence of conditional and generalized term rewriting systems, The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques, Applications and extensions of context-sensitive rewriting, Term orderings for non-reachability of (conditional) rewriting, Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)

Uses Software

• ELAN
• Haskell
• OBJ3
• CafeOBJ
• Maude
• Conditional Confluence

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Dependency pairs for proving termination properties of conditional term rewriting systems
• Normal forms and normal theories in conditional rewriting
• Semi-unification
• Mechanizing and improving dependency pairs
• A rationale for conditional equational programming
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Operational termination of conditional term rewriting systems
• Conditional rewrite rules
• Conditional rewrite rules: Confluence and termination
• Automatic synthesis of logical models for order-sorted first-order theories
• Analysis of rewriting-based systems as first-order theories
• Use of logical models for proving infeasibility in term rewriting
• Termination of term rewriting using dependency pairs
• 2D Dependency Pairs for Proving Operational Termination of CTRSs
• Extending the 2D Dependency Pair Framework for Conditional Term Rewriting Systems
• Proving Termination Properties with mu-term
• Theory of Formal Systems. (AM-47)
• Conditional Confluence (System Description)
• Frontiers of Combining Systems
• Logic for Programming, Artificial Intelligence, and Reasoning
• Rewriting Techniques and Applications
• Verification of Erlang processes by dependency pairs