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
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
- 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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
