KBO orientability
From MaRDI portal
Recommendations
Cites work
- A new polynomial-time algorithm for linear programming
- A structure-preserving clause form translation
- Arctic Termination ...Below Zero
- Automating the dependency pair method
- Automating the Knuth Bendix ordering
- Constraints for Argument Filterings
- Derivation lengths and order types of Knuth--Bendix orders
- Derivational Complexity of Knuth-Bendix Orders Revisited
- Frontiers of Combining Systems
- scientific article; zbMATH DE number 3644821 (Why is no real title available?)
- scientific article; zbMATH DE number 5139161 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- Increasing Interpretations
- Logic for Programming, Artificial Intelligence, and Reasoning
- Logic Programming
- Matrix interpretations for proving termination of term rewriting
- Maximal Termination
- Mechanizing and improving dependency pairs
- Orienting rewrite rules with the Knuth-Bendix order.
- Predictive Labeling with Dependency Pairs Using SAT
- Proving Termination Using Recursive Path Orders and SAT Solving
- SAT Solving for Argument Filterings
- SAT Solving for Termination Analysis with Polynomial Interpretations
- Satisfying KBO Constraints
- Search Techniques for Rational Polynomial Orders
- Solving Partial Order Constraints for LPO Termination
- Term Rewriting and All That
- Termination by Quasi-periodic Interpretations
- Termination of term rewriting using dependency pairs
- Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths
- Theory and Applications of Satisfiability Testing
- Tyrolean termination tool: techniques and features
Cited in
(20)- Orienting rewrite rules with the Knuth-Bendix order.
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- SAT solving for termination proofs with recursive path orders and dependency pairs
- scientific article; zbMATH DE number 1722704 (Why is no real title available?)
- Ordinals and Knuth-Bendix orders
- Encoding dependency pair techniques and control strategies for maximal completion
- Proving termination by dependency pairs and inductive theorem proving
- Decreasing diagrams and relative termination
- AC-KBO revisited
- On transfinite Knuth-Bendix orders
- Derivational Complexity of Knuth-Bendix Orders Revisited
- Satisfying KBO Constraints
- Decreasing diagrams and relative termination
- Weighted Path Orders Are Semantic Path Orders
- Certifying the weighted path order (invited talk)
- Lexicographic combination of reduction pairs
- Inferring RPO symbol orderings
- A Formalization of Knuth–Bendix Orders
- A Formalization of Weighted Path Orders and Recursive Path Orders
- Things to know when implementing KBO
This page was built for publication: KBO orientability
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q846165)
