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
- 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
- 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?)
- 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
(45)- 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
- Use of logical models for proving infeasibility in term rewriting
- Determinization of conditional term rewriting systems
- Twenty years of rewriting logic
- On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
- Determinization of inverted grammar programs via context-free expressions
- Applications and extensions of context-sensitive rewriting
- Stability of termination and sufficient-completeness under pushouts via amalgamation
- The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
- Proving operational termination of membership equational programs
- Proving semantic properties as first-order satisfiability
- Ground confluence of order-sorted conditional specifications modulo axioms
- Using well-founded relations for proving operational termination
- Automatic generation of logical models with AGES
- Methods for proving termination of rewriting-based programming languages by transformation
- Use of logical models for proving operational termination in general logics
- Transformation for refining unraveled conditional term rewriting systems
- Strong and weak operational termination of order-sorted rewrite theories
- 2D dependency pairs for proving operational termination of CTRSs
- Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude
- Rewriting strategies and strategic rewrite programs
- Extending the 2D dependency pair framework for conditional term rewriting systems
- Formalizing soundness and completeness of unravelings
- Complexity of conditional term rewriting
- Dependency pairs for proving termination properties of conditional term rewriting systems
- MTT: The Maude Termination Tool (System Description)
- Narrowing trees for syntactically deterministic conditional term rewriting systems
- Automatically Proving and Disproving Feasibility Conditions
- mu-term: Verify Termination Properties Automatically (System Description)
- 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
- On proving soundness of the computationally equivalent transformation for normal conditional term rewriting systems by using unravelings
- Localized operational termination in general logics
- Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications
- Local confluence of conditional and generalized term rewriting systems
- Strict coherence of conditional rewriting modulo axioms
- Wanda -- a higher-order termination tool (system description)
- Termination of generalized term rewriting systems
- Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification
- Characterizing and proving operational termination of deterministic conditional term rewriting systems
- Normal forms and normal theories in conditional rewriting
- An Isabelle/HOL formalization of semi-Thue and conditional semi-Thue systems
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)
