The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
From MaRDI portal
Publication:2228436
DOI10.1007/s10817-020-09542-3zbMath1459.68092OpenAlexW2999233193WikidataQ126346956 ScholiaQ126346956MaRDI QIDQ2228436
Raúl Gutiérrez, José Meseguer, Salvador Lucas
Publication date: 17 February 2021
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-020-09542-3
Related Items (3)
Automatically Proving and Disproving Feasibility Conditions ⋮ Applications and extensions of context-sensitive rewriting ⋮ Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Dependency pairs for proving termination properties of conditional term rewriting systems
- Characterizing and proving operational termination of deterministic conditional term rewriting systems
- Normal forms and normal theories in conditional rewriting
- Mechanically proving termination using polynomial interpretations
- Mechanizing and improving dependency pairs
- Matrix interpretations for proving termination of term rewriting
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Operational termination of conditional term rewriting systems
- A note on simplification orderings
- The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors
- Automatic synthesis of logical models for order-sorted first-order theories
- Use of logical models for proving infeasibility in term rewriting
- Termination of term rewriting using dependency pairs
- Using well-founded relations for proving operational termination
- Automatic generation of logical models with AGES
- 2D Dependency Pairs for Proving Operational Termination of CTRSs
- Extending the 2D Dependency Pair Framework for Conditional Term Rewriting Systems
- Proving Termination Properties with mu-term
- MTT: The Maude Termination Tool (System Description)
- Conditional Confluence (System Description)
- Automated Reasoning
- Applications of Strict Π11 predicates to infinitary logic
- Logic for Programming, Artificial Intelligence, and Reasoning
- Logic of many-sorted theories
- Rewriting Techniques and Applications
This page was built for publication: The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
