Proving weak properties of rewriting
From MaRDI portal
Publication:554217
DOI10.1016/j.tcs.2011.04.028zbMath1234.68178OpenAlexW2083907114MaRDI QIDQ554217
Isabelle Gnaedig, Hélène Kirchner
Publication date: 29 July 2011
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2011.04.028
Related Items (2)
A proof method for local sufficient completeness of term rewriting systems ⋮ A Finite Representation of the Narrowing Space
Uses Software
Cites Work
- Sufficient completeness verification for conditional and constrained TRS
- Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness
- On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems
- Using induction and rewriting to verify and complete parameterized specifications
- Testing for the ground (co-)reducibility property in term-rewriting systems
- Proofs by induction in equational theories with constructors
- On sufficient-completeness and related properties of term rewriting systems
- Completeness results for basic narrowing
- Maude: specification and programming in rewriting logic
- Automatic proofs by induction in theories without constructors
- Ground reducibility is EXPTIME-complete
- Induction for termination with local strategies
- Termination of rewriting under strategies
- Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations
- Semantic confluence tests and completion methods
- Proving innermost normalisation automatically
- Encompassment properties and automata with constraints
- Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
- Theoretical Aspects of Computing - ICTAC 2004
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Proving weak properties of rewriting