Term orderings for non-reachability of (conditional) rewriting

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

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)

Cites Work

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

Cited In (8)

• Rewriting with a nondeterministic choice operator
• Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
• NaTT
• Could orders be captured by term rewriting systems?
• Termination orderings for associative-commutative rewriting systems
• Title not available (Why is that?)
• Weighted Path Orders Are Semantic Path Orders
• Bi-rewriting, a term rewriting technique for monotonic order relations

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2104512)