Nagoya termination tool

DOI10.1007/978-3-319-08918-8_32MaRDI QIDQ5170837zbMATH OpenOpenAlexFDO

Authors Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe

Publication date 24 July 2014

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1404.6626

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Abstract: This paper describes the implementation and techniques of the Nagoya Termination Tool, a termination prover for term rewrite systems. The main features of the tool are: the first implementation of the weighted path order which subsumes most of the existing reduction pairs, and the efficiency due to the strong cooperation with external SMT solvers. We present some new ideas that contribute to the efficiency and power of the tool.

Recommendations

• scientific article; zbMATH DE number 2043537
• Tyrolean termination tool: techniques and features
• Term Rewriting and Applications
• Proving termination properties with \textsc{mu-term}
• scientific article; zbMATH DE number 3930339

Cited in

(24)

• Multi-dimensional interpretations for termination of term rewriting
• Tuple interpretations for termination of term rewriting
• Term orderings for non-reachability of (conditional) rewriting
• Automated termination analysis of polynomial probabilistic programs
• Confluence by critical pair analysis revisited
• Relative termination via dependency pairs
• Nagoya Termination Tool
• Encoding dependency pair techniques and control strategies for maximal completion
• Reducing relative termination to dependency pair problems
• MTT: The Maude Termination Tool (System Description)
• scientific article; zbMATH DE number 2043537 (Why is no real title available?)
• Satisfiability checking: theory and applications
• Term Rewriting and Applications
• Compositional confluence criteria
• Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
• Left-Linear Completion with AC Axioms
• Weighted Path Orders Are Semantic Path Orders
• From innermost to full almost-sure termination of probabilistic term rewriting
• Certifying the weighted path order (invited talk)
• From innermost to full probabilistic term rewriting: almost-sure termination, complexity, and modularity
• Lexicographic combination of reduction pairs
• Left-linear completion with AC axioms
• A dependency pair framework for relative termination of term rewriting
• Tyrolean termination tool: techniques and features

Describes a project that uses

Uses Software

• NaTT

This page was built for publication: Nagoya termination tool

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