Term orderings for non-reachability of (conditional) rewriting

DOI10.1007/978-3-031-10769-6_15OpenAlexW4289104053MaRDI QIDQ2104512

Akihisa Yamada

Publication date: 7 December 2022

Full work available at URL: https://doi.org/10.1007/978-3-031-10769-6_15

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

NaTT

Uses Software

• z3
• Timbuk
• Tyrolean
• AProVE
• StarExec
• MU-TERM
• Nagoya Termination Tool

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Dependency pairs for proving termination properties of conditional term rewriting systems
• Reachability analysis over term rewriting systems
• Orderings for term-rewriting systems
• Mechanizing and improving dependency pairs
• Matrix interpretations for proving termination of term rewriting
• The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors
• Use of logical models for proving infeasibility in term rewriting
• Termination of term rewriting using dependency pairs
• Multi-dimensional interpretations for termination of term rewriting
• Automating the dependency pair method
• Disproving Confluence of Term Rewriting Systems by Interpretation and Ordering
• 2D Dependency Pairs for Proving Operational Termination of CTRSs
• Proving Termination of Programs Automatically with AProVE
• Term Rewriting and All That
• Automatically Proving and Disproving Feasibility Conditions
• mu-term: Verify Termination Properties Automatically (System Description)
• Nagoya Termination Tool
• Functional and Logic Programming
• The termination hierarchy for term rewriting
• Reachability Analysis for Termination and Confluence of Rewriting
• Tuple Interpretations for Higher-Order Complexity.

This page was built for publication: Term orderings for non-reachability of (conditional) rewriting