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

DOI10.1007/978-3-540-70590-1_7MaRDI QIDQ3522011zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Operational termination of conditional rewriting with built-in numbers and semantic data structures
• Termination of Context-Sensitive Rewriting with Built-In Numbers and Collection Data Structures
• Dependency Pairs for Rewriting with Non-free Constructors
• scientific article; zbMATH DE number 1722701
• Proving Termination of Integer Term Rewriting

Cites work

• Complete Sets of Reductions for Some Equational Theories
• Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
• Dependency Pairs for Rewriting with Non-free Constructors
• Frontiers of Combining Systems
• scientific article; zbMATH DE number 1722701 (Why is no real title available?)
• scientific article; zbMATH DE number 1487842 (Why is no real title available?)
• Logic for Programming, Artificial Intelligence, and Reasoning
• Mechanically proving termination using polynomial interpretations
• Mechanizing and improving dependency pairs
• Modular and incremental proofs of AC-termination
• Normalized rewriting: An alternative to rewriting modulo a set of equations
• On the Implementation of Construction Functions for Non-free Concrete Data Types
• Operational termination of conditional rewriting with built-in numbers and semantic data structures
• Proving Termination by Bounded Increase
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Termination of term rewriting using dependency pairs
• Tyrolean termination tool: techniques and features

Cited in

(15)

• Applications and extensions of context-sensitive rewriting
• Generalized rewrite theories, coherence completion, and symbolic methods
• scientific article; zbMATH DE number 1722701 (Why is no real title available?)
• Rewriting modulo SMT and open system analysis
• Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
• Termination of Context-Sensitive Rewriting with Built-In Numbers and Collection Data Structures
• Proving Termination of Integer Term Rewriting
• Completion for logically constrained rewriting
• 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
• Datatype defining rewrite systems for naturals and integers
• Operationally-based program equivalence proofs using LCTRSs
• Proving confluence in the confluence framework with confident
• Transforming concurrent programs with semaphores into logically constrained term rewrite systems

Describes a project that uses

Uses Software

• AProVE
• Tyrolean

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3522011)