Operational termination of conditional term rewriting systems
From MaRDI portal
Recommendations
- Characterizing and proving operational termination of deterministic conditional term rewriting systems
- Dependency pairs for proving termination properties of conditional term rewriting systems
- 2D dependency pairs for proving operational termination of CTRSs
- Strong and weak operational termination of order-sorted rewrite theories
- Sufficient conditions for modular termination of conditional term rewriting systems
Cites work
- scientific article; zbMATH DE number 1729952 (Why is no real title available?)
- scientific article; zbMATH DE number 1189278 (Why is no real title available?)
- scientific article; zbMATH DE number 2038715 (Why is no real title available?)
- scientific article; zbMATH DE number 1405447 (Why is no real title available?)
- A rationale for conditional equational programming
- CafeOBJ Report. The language, proof techniques, and methodologies for object-oriented algebraicspecification
- Conditional rewrite rules
- Conditional rewrite rules: Confluence and termination
- ELAN from a rewriting logic point of view
- Maude: specification and programming in rewriting logic
- Simplifying conditional term rewriting systems: Unification, termination and confluence
- Specification and proof in membership equational logic
- Unravelings and ultra-properties
Cited in
(44)- 2D dependency pairs for proving operational termination of CTRSs
- Extending the 2D dependency pair framework for conditional term rewriting systems
- Operational termination of conditional rewriting with built-in numbers and semantic data structures
- Twenty years of rewriting logic
- Operational termination of membership equational programs: the order-sorted way
- Strict coherence of conditional rewriting modulo axioms
- Stability of termination and sufficient-completeness under pushouts via amalgamation
- Automatic generation of logical models with AGES
- Automatically Proving and Disproving Feasibility Conditions
- mu-term: Verify Termination Properties Automatically (System Description)
- Ground confluence of order-sorted conditional specifications modulo axioms
- Proving operational termination of membership equational programs
- On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings
- Local confluence of conditional and generalized term rewriting systems
- Using well-founded relations for proving operational termination
- Rewriting strategies and strategic rewrite programs
- Automatic synthesis of logical models for order-sorted first-order theories
- Complexity of conditional term rewriting
- Formalizing soundness and completeness of unravelings
- Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification
- Determinization of conditional term rewriting systems
- On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
- The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors
- Use of logical models for proving infeasibility in term rewriting
- MTT: The Maude Termination Tool (System Description)
- Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude
- Applications and extensions of context-sensitive rewriting
- Sentence-normalized conditional narrowing modulo in rewriting logic and Maude
- Narrowing trees for syntactically deterministic conditional term rewriting systems
- Use of logical models for proving operational termination in general logics
- Methods for proving termination of rewriting-based programming languages by transformation
- The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
- Wanda -- a higher-order termination tool (system description)
- Strong and weak operational termination of order-sorted rewrite theories
- Localized operational termination in general logics
- Dependency pairs for proving termination properties of conditional term rewriting systems
- Termination of generalized term rewriting systems
- Transformation for refining unraveled conditional term rewriting systems
- Proving semantic properties as first-order satisfiability
- Characterizing and proving operational termination of deterministic conditional term rewriting systems
- Normal forms and normal theories in conditional rewriting
- Completion after program inversion of injective functions
- Determinization of inverted grammar programs via context-free expressions
- Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications
This page was built for publication: Operational termination of conditional term rewriting systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1041807)
