KBO orientability
From MaRDI portal
Publication:846165
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
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
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
