Search Techniques for Rational Polynomial Orders

DOI10.1007/978-3-540-85110-3_10zbMath1166.68354OpenAlexW1543075099MaRDI QIDQ5505493

Carsten Otto, Salvador Lucas, Carsten Fuhs, Peter Schneider-Kamp, Rafael Navarro-Marset, Jürgen Giesl

Publication date: 27 January 2009

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

Full work available at URL: https://doi.org/10.1007/978-3-540-85110-3_10

zbMATH Keywords

terminationterm rewritingSAT solvingdependency pairs

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Grammars and rewriting systems (68Q42)

Related Items

Analyzing program termination and complexity automatically with \textsf{AProVE}, KBO orientability, SAT solving for termination proofs with recursive path orders and dependency pairs, Size-based termination of higher-order rewriting, SAT modulo linear arithmetic for solving polynomial constraints, Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic, Increasing interpretations

Uses Software

• MU-TERM
• Jambox

Cites Work

• Mechanically proving termination using polynomial interpretations
• Tyrolean termination tool: techniques and features
• Mechanizing and improving dependency pairs
• Termination of rewriting
• Testing positiveness of polynomials
• Termination of term rewriting using dependency pairs
• Automating the dependency pair method
• On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting
• Innermost Termination of Rewrite Systems by Labeling
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Matrix Interpretations for Proving Termination of Term Rewriting
• Polynomials over the reals in proofs of termination : from theory to practice
• Logic for Programming, Artificial Intelligence, and Reasoning