Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures

DOI10.1007/978-3-540-70590-1_7zbMath1145.68445OpenAlexW1496435538MaRDI QIDQ3522011

Stephan Falke, Deepak Kapur

Publication date: 28 August 2008

Published in: Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-70590-1_7

Mathematics Subject Classification ID

Searching and sorting (68P10) Grammars and rewriting systems (68Q42)

Related Items (10)

Rewriting modulo SMT and open system analysis ⋮ Operationally-based program equivalence proofs using LCTRSs ⋮ Unnamed Item ⋮ Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures ⋮ Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures ⋮ A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs ⋮ On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs ⋮ Generalized rewrite theories, coherence completion, and symbolic methods ⋮ Applications and extensions of context-sensitive rewriting ⋮ Proving Termination of Integer Term Rewriting

Uses Software

• Tyrolean
• AProVE

Cites Work

• Unnamed Item
• Unnamed Item
• Mechanically proving termination using polynomial interpretations
• Tyrolean termination tool: techniques and features
• Mechanizing and improving dependency pairs
• Termination of term rewriting using dependency pairs
• Normalized rewriting: An alternative to rewriting modulo a set of equations
• Modular and incremental proofs of AC-termination
• Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
• Dependency Pairs for Rewriting with Non-free Constructors
• Proving Termination by Bounded Increase
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Complete Sets of Reductions for Some Equational Theories
• Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures
• Frontiers of Combining Systems
• Logic for Programming, Artificial Intelligence, and Reasoning
• On the Implementation of Construction Functions for Non-free Concrete Data Types

This page was built for publication: Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures