Maximal Termination

DOI10.1007/978-3-540-70590-1_8MaRDI QIDQ3522012zbMATH OpenOpenAlexFDO

Authors Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, Harald Zankl

Publication date 28 August 2008

Published in Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-70590-1_8

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• SAT Solving for Termination Analysis with Polynomial Interpretations
• Mechanically proving termination using polynomial interpretations
• Matrix interpretations for proving termination of term rewriting
• Matrix Interpretations for Proving Termination of Term Rewriting
• Search Techniques for Rational Polynomial Orders

Cites work

• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• Automating the dependency pair method
• Counterexamples to termination for the direct sum of term rewriting systems
• Logic for Programming, Artificial Intelligence, and Reasoning
• Maximal Termination
• Mechanizing and improving dependency pairs
• Polytool: polynomial interpretations as a basis for termination analysis of logic programs
• Proof of termination of the rewriting system SUBSET on CCL
• Proving Termination by Bounded Increase
• SAT Solving for Termination Analysis with Polynomial Interpretations
• TPA: Termination Proved Automatically
• Termination of term rewriting using dependency pairs
• Testing positiveness of polynomials
• Tyrolean termination tool: techniques and features

Cited in

(20)

• On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs
• On complexity bounds and confluence of parallel term rewriting
• KBO orientability
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Monotonicity criteria for polynomial interpretations over the naturals
• Increasing interpretations
• Outermost ground termination
• Increasing Interpretations
• Maximal Termination
• Analysing parallel complexity of term rewriting
• SAT solving for termination proofs with recursive path orders and dependency pairs
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Automatic proofs of termination with elementary interpretations
• Proving Termination of Integer Term Rewriting
• Tuple interpretations for termination of term rewriting
• Automatic synthesis of logical models for order-sorted first-order theories
• Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
• Ramsey versus lexicographic termination proving
• Automated Implicit Computational Complexity Analysis (System Description)
• Multi-dimensional interpretations for termination of term rewriting

This page was built for publication: Maximal Termination

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3522012)