KBO orientability

DOI10.1007/s10817-009-9131-zzbMath1184.68303OpenAlexW2913313741MaRDI QIDQ846165

Aart Middeldorp, Nao Hirokawa, Harald Zankl

Publication date: 1 February 2010

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

Full work available at URL: https://doi.org/10.1007/s10817-009-9131-z

zbMATH Keywords

terminationterm rewritingKnuth-Bendix order

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (8)

Analyzing program termination and complexity automatically with \textsf{AProVE} ⋮ Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion ⋮ SAT solving for termination proofs with recursive path orders and dependency pairs ⋮ AC-KBO revisited ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ Decreasing diagrams and relative termination ⋮ Decreasing Diagrams and Relative Termination ⋮ On Transfinite Knuth-Bendix Orders

Uses Software

• MiniSat
• Tyrolean
• AProVE
• TPDB

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths
• Automating the Knuth Bendix ordering
• A new polynomial-time algorithm for linear programming
• Tyrolean termination tool: techniques and features
• Mechanizing and improving dependency pairs
• Matrix interpretations for proving termination of term rewriting
• A structure-preserving clause form translation
• Orienting rewrite rules with the Knuth-Bendix order.
• Termination of term rewriting using dependency pairs
• Automating the dependency pair method
• Maximal Termination
• Arctic Termination ...Below Zero
• Proving Termination Using Recursive Path Orders and SAT Solving
• Solving Partial Order Constraints for LPO Termination
• Predictive Labeling with Dependency Pairs Using SAT
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Term Rewriting and All That
• Logic Programming
• Theory and Applications of Satisfiability Testing
• SAT Solving for Argument Filterings
• Derivational Complexity of Knuth-Bendix Orders Revisited
• Satisfying KBO Constraints
• Termination by Quasi-periodic Interpretations
• Constraints for Argument Filterings
• Frontiers of Combining Systems
• Search Techniques for Rational Polynomial Orders
• Increasing Interpretations
• Logic for Programming, Artificial Intelligence, and Reasoning
• Derivation lengths and order types of Knuth--Bendix orders

This page was built for publication: KBO orientability