Tyrolean termination tool: techniques and features

DOI10.1016/j.ic.2006.08.010zbMath1111.68048OpenAlexW2164290630MaRDI QIDQ876042

Nao Hirokawa, Aart Middeldorp

Publication date: 16 April 2007

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2006.08.010

zbMATH Keywords

terminationterm rewritingautomationpolynomial interpretationsdependency pair method

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (38)

Relative termination via dependency pairs ⋮ Harnessing First Order Termination Provers Using Higher Order Dependency Pairs ⋮ Transforming orthogonal inductive definition sets into confluent term rewrite systems ⋮ KBO orientability ⋮ Certification of Termination Proofs Using CeTA ⋮ SAT solving for termination proofs with recursive path orders and dependency pairs ⋮ Dependency pairs for proving termination properties of conditional term rewriting systems ⋮ Uncurrying for termination and complexity ⋮ Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures ⋮ Maximal Termination ⋮ Usable Rules for Context-Sensitive Rewrite Systems ⋮ Arctic Termination ...Below Zero ⋮ Deciding Innermost Loops ⋮ Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems ⋮ Automated Complexity Analysis Based on the Dependency Pair Method ⋮ Loop detection in term rewriting using the eliminating unfoldings ⋮ Monotonicity Criteria for Polynomial Interpretations over the Naturals ⋮ From Outermost Termination to Innermost Termination ⋮ A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs ⋮ Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic ⋮ Termination Analysis by Dependency Pairs and Inductive Theorem Proving ⋮ Beyond Dependency Graphs ⋮ Unnamed Item ⋮ Context-sensitive dependency pairs ⋮ Certification of Proving Termination of Term Rewriting by Matrix Interpretations ⋮ On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs ⋮ Methods for Proving Termination of Rewriting-based Programming Languages by Transformation ⋮ Proving Termination of Integer Term Rewriting ⋮ CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates ⋮ The Derivational Complexity Induced by the Dependency Pair Method ⋮ Argument Filterings and Usable Rules for Simply Typed Dependency Pairs ⋮ Match-bounds revisited ⋮ Increasing interpretations ⋮ Search Techniques for Rational Polynomial Orders ⋮ Increasing Interpretations ⋮ Innermost Termination of Rewrite Systems by Labeling

Uses Software

• Tyrolean
• AProVE
• TPDB
• TPA
• Matchbox
• Tsukuba

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Automating the Knuth Bendix ordering
• Mechanically proving termination using polynomial interpretations
• Counterexamples to termination for the direct sum of term rewriting systems
• Testing positiveness of polynomials
• Generalized sufficient conditions for modular termination of rewriting
• Orienting rewrite rules with the Knuth-Bendix order.
• Type introduction for equational rewriting
• Modular termination proofs for rewriting using dependency pairs
• Termination of term rewriting using dependency pairs
• Automating the dependency pair method
• The size-change principle and dependency pairs for termination of term rewriting
• Modular and incremental automated termination proofs
• TPA: Termination Proved Automatically
• Matrix Interpretations for Proving Termination of Term Rewriting
• Automated Reasoning
• Foundations of Software Science and Computation Structures
• Logic Programming
• Polynomials over the reals in proofs of termination : from theory to practice
• Artificial Intelligence and Symbolic Computation
• Term Rewriting and Applications
• Term Rewriting and Applications
• Term Rewriting and Applications
• Rewriting Techniques and Applications

This page was built for publication: Tyrolean termination tool: techniques and features