Tuple interpretations for termination of term rewriting

DOI10.1007/S10817-022-09640-4OpenAlexW4287577798MaRDI QIDQ2102931FDOQ2102931

Authors: Akihisa Yamada 

Publication date: 12 December 2022

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-022-09640-4

Recommendations

• Termination of term rewriting by interpretation
• Increasing Interpretations
• Matrix interpretations for proving termination of term rewriting
• Matrix Interpretations for Proving Termination of Term Rewriting
• Improved matrix interpretation

zbMATH Keywords

algebraterm rewritingterminationinterpretation method

Mathematics Subject Classification ID

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

Cites Work

• Certification of Termination Proofs Using CeTA
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
• Nagoya termination tool
• Termination of term rewriting: Interpretation and type elimination
• The termination hierarchy for term rewriting
• Termination of term rewriting using dependency pairs
• Rewriting Techniques and Applications
• Term Rewriting and All That
• Satisfiability modulo theories
• Multi-dimensional interpretations for termination of term rewriting
• Title not available (Why is that?)
• Logic for Programming, Artificial Intelligence, and Reasoning
• Mechanizing and improving dependency pairs
• Matrix interpretations for proving termination of term rewriting
• Automatic synthesis of logical models for order-sorted first-order theories
• Artificial Intelligence and Symbolic Computation
• Automated certified proofs with CiME3
• Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
• Termination of String Rewriting with Matrix Interpretations
• Maximal Termination
• A SAT-Based Approach to Size Change Termination with Global Ranking Functions
• Improved matrix interpretation
• mu-term: Verify Termination Properties Automatically (System Description)
• Max/Plus tree automata for termination of term rewriting
• Dynamic dependency pairs for algebraic functional systems
• Tuple Interpretations for Higher-Order Complexity.

Cited In (3)

• Increasing Interpretations
• Increasing interpretations
• Analyzing Innermost Runtime Complexity Through Tuple Interpretations

Uses Software

• z3
• CeTA
• Tyrolean
• AProVE
• CoLoR
• CiME
• MU-TERM
• TPDB
• Nagoya Termination Tool
• NaTT

This page was built for publication: Tuple interpretations for termination of term rewriting

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