Operational termination of conditional term rewriting systems
From MaRDI portal
Publication:1041807
DOI10.1016/J.IPL.2005.05.002zbMath1185.68374OpenAlexW2091448415MaRDI QIDQ1041807
José Meseguer, Claude Marché, Salvador Lucas
Publication date: 4 December 2009
Published in: Information Processing Letters (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ipl.2005.05.002
Related Items (38)
Unnamed Item ⋮ Automatically Proving and Disproving Feasibility Conditions ⋮ mu-term: Verify Termination Properties Automatically (System Description) ⋮ The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors ⋮ Sentence-normalized conditional narrowing modulo in rewriting logic and Maude ⋮ Automatic synthesis of logical models for order-sorted first-order theories ⋮ Dependency pairs for proving termination properties of conditional term rewriting systems ⋮ Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude ⋮ Rewriting Strategies and Strategic Rewrite Programs ⋮ Determinization of conditional term rewriting systems ⋮ Twenty years of rewriting logic ⋮ On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories ⋮ Local confluence of conditional and generalized term rewriting systems ⋮ Formalizing Soundness and Completeness of Unravelings ⋮ On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings ⋮ Stability of termination and sufficient-completeness under pushouts via amalgamation ⋮ MTT: The Maude Termination Tool (System Description) ⋮ Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems ⋮ The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques ⋮ Determinization of inverted grammar programs via context-free expressions ⋮ Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications ⋮ Strict coherence of conditional rewriting modulo axioms ⋮ Use of logical models for proving infeasibility in term rewriting ⋮ Completion after Program Inversion of Injective Functions ⋮ Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures ⋮ Operational Termination of Membership Equational Programs: the Order-Sorted Way ⋮ Characterizing and proving operational termination of deterministic conditional term rewriting systems ⋮ Proving operational termination of membership equational programs ⋮ Normal forms and normal theories in conditional rewriting ⋮ Proving semantic properties as first-order satisfiability ⋮ Ground confluence of order-sorted conditional specifications modulo axioms ⋮ Applications and extensions of context-sensitive rewriting ⋮ Methods for Proving Termination of Rewriting-based Programming Languages by Transformation ⋮ Using well-founded relations for proving operational termination ⋮ Automatic generation of logical models with AGES ⋮ Use of Logical Models for Proving Operational Termination in General Logics ⋮ Localized Operational Termination in General Logics ⋮ Transformation for Refining Unraveled Conditional Term Rewriting Systems
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A rationale for conditional equational programming
- Conditional rewrite rules
- Simplifying conditional term rewriting systems: Unification, termination and confluence
- Conditional rewrite rules: Confluence and termination
- ELAN from a rewriting logic point of view
- Maude: specification and programming in rewriting logic
- Specification and proof in membership equational logic
- Unravelings and ultra-properties
This page was built for publication: Operational termination of conditional term rewriting systems
