Polynomials over the reals in proofs of termination : from theory to practice

DOI10.1051/ita:2005029zbMath1085.68076OpenAlexW1978221548MaRDI QIDQ5313720

Salvador Lucas

Publication date: 1 September 2005

Published in: RAIRO - Theoretical Informatics and Applications (Search for Journal in Brave)

Full work available at URL: http://www.numdam.org/item?id=ITA_2005__39_3_547_0

zbMATH Keywords

polynomial algebrasterm rewritingconstraint-solving systems

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Grammars and rewriting systems (68Q42)

Related Items (17)

Proving termination of context-sensitive rewriting by transformation ⋮ Automatic synthesis of logical models for order-sorted first-order theories ⋮ Tyrolean termination tool: techniques and features ⋮ Mechanizing and improving dependency pairs ⋮ Size-based termination of higher-order rewriting ⋮ Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting ⋮ SAT modulo linear arithmetic for solving polynomial constraints ⋮ Automatic Proofs of Termination With Elementary Interpretations ⋮ Monotonicity Criteria for Polynomial Interpretations over the Naturals ⋮ 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 ⋮ Context-sensitive dependency pairs ⋮ Proving Termination Properties with mu-term ⋮ Use of Logical Models for Proving Operational Termination in General Logics ⋮ Derivational complexity and context-sensitive Rewriting ⋮ Search Techniques for Rational Polynomial Orders ⋮ Proving Termination of Context-Sensitive Rewriting with MU-TERM

Uses Software

• Tyrolean
• AProVE
• CiME
• MU-TERM
• REVE

Cites Work

• Termination of rewriting systems by polynomial interpretations and its implementation
• Orderings for term-rewriting systems
• Relaxing monotonicity for innermost termination
• Mechanically proving termination using polynomial interpretations
• Proving termination of context-sensitive rewriting by transformation
• Termination of rewriting
• A note on simplification orderings
• Rewrite, rewrite, rewrite, rewrite, rewrite, \dots
• Simulation of Turing machines by a regular rewrite rule
• Testing positiveness of polynomials
• Generating polynomial orderings
• Context-sensitive rewriting strategies
• Modular termination proofs for rewriting using dependency pairs
• Total termination of term rewriting is undecidable
• Termination of term rewriting using dependency pairs
• Termination of context-sensitive rewriting
• Term Rewriting and All That
• Automated Reasoning
• Artificial Intelligence and Symbolic Computation
• Transformation techniques for context-sensitive rewrite systems
• Term Rewriting and Applications
• Rewriting Techniques and Applications
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Polynomials over the reals in proofs of termination : from theory to practice