Automatically Proving and Disproving Feasibility Conditions
From MaRDI portal
Publication:5049020
DOI10.1007/978-3-030-51054-1_27OpenAlexW3040061435MaRDI QIDQ5049020
Raúl Gutiérrez, Salvador Lucas
Publication date: 9 November 2022
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-030-51054-1_27
Related Items (4)
mu-term: Verify Termination Properties Automatically (System Description) ⋮ Local confluence of conditional and generalized term rewriting systems ⋮ Applications and extensions of context-sensitive rewriting ⋮ Term orderings for non-reachability of (conditional) rewriting
Uses Software
Cites Work
- Mechanizing and improving dependency pairs
- Operational termination of conditional term rewriting systems
- Termination of rewriting
- The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors
- Analysis of rewriting-based systems as first-order theories
- Over-approximating terms reachable by context-sensitive rewriting
- Use of logical models for proving infeasibility in term rewriting
- MædMax: a maximal ordered completion tool
- The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
- Proving semantic properties as first-order satisfiability
- Using well-founded relations for proving operational termination
- Automatic generation of logical models with AGES
- Innermost Reachability and Context Sensitive Reachability Properties Are Decidable for Linear Right-Shallow Term Rewriting Systems
- Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems
- Reachability Analysis for Termination and Confluence of Rewriting
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Automatically Proving and Disproving Feasibility Conditions
