Tyrolean termination tool: techniques and features
From MaRDI portal
Publication:876042
DOI10.1016/J.IC.2006.08.010zbMATH Open1111.68048OpenAlexW2164290630MaRDI QIDQ876042FDOQ876042
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
Recommendations
Cites Work
- TPA: Termination Proved Automatically
- Modular termination proofs for rewriting using dependency pairs
- Termination of term rewriting using dependency pairs
- Title not available (Why is that?)
- Rewriting Techniques and Applications
- Types and programing languages
- Title not available (Why is that?)
- Automating the dependency pair method
- Title not available (Why is that?)
- Logic Programming
- Term Rewriting and Applications
- Counterexamples to termination for the direct sum of term rewriting systems
- Polynomials over the reals in proofs of termination : from theory to practice
- Mechanically proving termination using polynomial interpretations
- Testing positiveness of polynomials
- Artificial Intelligence and Symbolic Computation
- Term Rewriting and Applications
- Title not available (Why is that?)
- Title not available (Why is that?)
- Generalized sufficient conditions for modular termination of rewriting
- Title not available (Why is that?)
- Term Rewriting and Applications
- Automating the Knuth Bendix ordering
- Automated Reasoning
- Foundations of Software Science and Computation Structures
- Orienting rewrite rules with the Knuth-Bendix order.
- Modular and incremental automated termination proofs
- Title not available (Why is that?)
- Type introduction for equational rewriting
- The size-change principle and dependency pairs for termination of term rewriting
- Approximations for strategies and termination
- Matrix Interpretations for Proving Termination of Term Rewriting
Cited In (43)
- Title not available (Why is that?)
- Match-bounds revisited
- Title not available (Why is that?)
- Certification of Proving Termination of Term Rewriting by Matrix Interpretations
- Increasing Interpretations
- Uncurrying for termination and complexity
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
- Certification of Termination Proofs Using CeTA
- Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems
- Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting
- The Derivational Complexity Induced by the Dependency Pair Method
- Beyond Dependency Graphs
- Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
- Termination Analysis by Dependency Pairs and Inductive Theorem Proving
- TPA: Termination Proved Automatically
- Proving termination by dependency pairs and inductive theorem proving
- Search Techniques for Rational Polynomial Orders
- Argument filterings and usable rules for simply typed dependency pairs
- Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
- MTT: The Maude Termination Tool (System Description)
- Relative termination via dependency pairs
- KBO orientability
- Transforming orthogonal inductive definition sets into confluent term rewrite systems
- SAT solving for termination proofs with recursive path orders and dependency pairs
- Harnessing First Order Termination Provers Using Higher Order Dependency Pairs
- Deciding Innermost Loops
- Methods for proving termination of rewriting-based programming languages by transformation
- On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs
- Dependency pairs for proving termination properties of conditional term rewriting systems
- Proving Termination of Integer Term Rewriting
- Monotonicity Criteria for Polynomial Interpretations over the Naturals
- Increasing interpretations
- Tyrolean Complexity Tool: Features and Usage.
- Arctic Termination ...Below Zero
- Maximal Termination
- Usable Rules for Context-Sensitive Rewrite Systems
- Automated Complexity Analysis Based on the Dependency Pair Method
- Context-sensitive dependency pairs
- From Outermost Termination to Innermost Termination
- Loop detection in term rewriting using the eliminating unfoldings
- Term Rewriting and Applications
- Innermost termination of rewrite systems by labeling
- A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
Uses Software
This page was built for publication: Tyrolean termination tool: techniques and features
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q876042)
