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

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