Proving weak properties of rewriting

DOI10.1016/J.TCS.2011.04.028MaRDI QIDQ554217zbMATH OpenOpenAlexFDO

Authors 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

zbMATH Keywords

abstractioncompletenessinductionrewritingnarrowingweak termination

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Theoretical Aspects of Computing - ICTAC 2004
• scientific article; zbMATH DE number 3934390
• Termination of rewriting under strategies
• Termination of rewriting
• Termination of Priority Rewriting

Cites work

• scientific article; zbMATH DE number 3913659 (Why is no real title available?)
• scientific article; zbMATH DE number 4047063 (Why is no real title available?)
• scientific article; zbMATH DE number 4049024 (Why is no real title available?)
• scientific article; zbMATH DE number 3776841 (Why is no real title available?)
• scientific article; zbMATH DE number 1301734 (Why is no real title available?)
• scientific article; zbMATH DE number 1324443 (Why is no real title available?)
• scientific article; zbMATH DE number 1956456 (Why is no real title available?)
• scientific article; zbMATH DE number 1841839 (Why is no real title available?)
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• Automatic proofs by induction in theories without constructors
• Completeness results for basic narrowing
• Encompassment properties and automata with constraints
• Ground reducibility is EXPTIME-complete
• Improving dependency pairs
• Induction for termination with local strategies
• Inductionless induction
• Maude: specification and programming in rewriting logic
• Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations
• On sufficient-completeness and related properties of term rewriting systems
• On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems
• Outermost ground termination
• Proofs by induction in equational theories with constructors
• Proving innermost normalisation automatically
• Rewriting
• Semantic confluence tests and completion methods
• Sufficient completeness verification for conditional and constrained TRS
• Termination of rewriting under strategies
• Testing for the ground (co-)reducibility property in term-rewriting systems
• Theoretical Aspects of Computing - ICTAC 2004
• Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness
• Using induction and rewriting to verify and complete parameterized specifications
• Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture

Cited in

(3)

• A proof method for local sufficient completeness of term rewriting systems
• Theoretical Aspects of Computing - ICTAC 2004
• A Finite Representation of the Narrowing Space

Describes a project that uses

Uses Software

• CARIBOO
• Maude
• ELAN

This page was built for publication: Proving weak properties of rewriting

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