Mechanically proving termination using polynomial interpretations

DOI10.1007/s10817-005-9022-xzbMath1108.03017OpenAlexW1988455648MaRDI QIDQ851142

Claude Marché, Ana Paula Tomás, Evelyne Contejean, Xavier Urbain

Publication date: 17 November 2006

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

Full work available at URL: https://doi.org/10.1007/s10817-005-9022-x

zbMATH Keywords

terminationDiophantine constraintspolynomial interpretationspolynomial orderingsweakly monotonic orderings

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Related Items (24)

Mechanically proving termination using polynomial interpretations ⋮ Polynomials over the reals in proofs of termination : from theory to practice ⋮ Automatic synthesis of logical models for order-sorted first-order theories ⋮ Tyrolean termination tool: techniques and features ⋮ Size-based termination of higher-order rewriting ⋮ Analyzing Innermost Runtime Complexity Through Tuple Interpretations ⋮ SAT modulo linear arithmetic for solving polynomial constraints ⋮ Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures ⋮ Proving Quadratic Derivational Complexities Using Context Dependent Interpretations ⋮ Automated Implicit Computational Complexity Analysis (System Description) ⋮ Automated Complexity Analysis Based on the Dependency Pair Method ⋮ The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques ⋮ Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations ⋮ Monotonicity Criteria for Polynomial Interpretations over the Naturals ⋮ A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs ⋮ Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic ⋮ On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting ⋮ Complexity Analysis by Rewriting ⋮ CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates ⋮ Derivational complexity and context-sensitive Rewriting ⋮ Termination Analysis of Logic Programs Based on Dependency Graphs ⋮ Search Techniques for Rational Polynomial Orders ⋮ Modular and incremental automated termination proofs ⋮ Type-based analysis of logarithmic amortised complexity

Uses Software

• Mizar
• AProVE
• CiME
• CARIBOO
• Tsukuba
• REVE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Termination of rewriting systems by polynomial interpretations and its implementation
• Orderings for term-rewriting systems
• Mechanically proving termination using polynomial interpretations
• Theoretical computer science. Cumulative index, volumes 1-100 (1992)
• Testing positiveness of polynomials
• Efficient computation of addition chains
• Termination of rewrite systems by elementary interpretations
• Modular termination proofs for rewriting using dependency pairs
• Termination of term rewriting using dependency pairs
• Modular and incremental automated termination proofs
• Algorithms with polynomial interpretation termination proof
• Compiling constraints in clp(FD)
• Minimizing sums of addition chains
• Preuves de terminaison de systèmes de réécriture fondées sur les interprétations polynomiales. Une méthode basée sur le théorème de Sturm
• Addition Chain Methods for the Evaluation of Specific Polynomials
• On the Evaluation of Powers and Monomials
• Computing Sequences with Addition Chains
• On vectorial addition chains
• Term Rewriting and All That
• Addition chains using continued fractions

This page was built for publication: Mechanically proving termination using polynomial interpretations