20 papers:
PPDP-2013-YamadaKS #order #polynomial #recursion- Unifying the Knuth-Bendix, recursive path and polynomial orders (AY, KK, TS), pp. 181–192.
RTA-2013-SternagelT #formal method #order- Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion (CS, RT), pp. 287–302.
IJCAR-2012-SternagelZ #named #visualisation- KBCV — Knuth-Bendix Completion Visualizer (TS, HZ), pp. 530–536.
CADE-2011-KovacsMV #on the #order- On Transfinite Knuth-Bendix Orders (LK, GM, AV), pp. 384–399.
- RTA-2006-WehrmanSW #named #termination
- Slothrop: Knuth-Bendix Completion with a Modern Termination Checker (IW, AS, EMW), pp. 287–296.
- CADE-2005-ZhangSM #decidability #first-order
- The Decidability of the First-Order Theory of Knuth-Bendix Order (TZ, HBS, ZM), pp. 131–148.
- CADE-2003-KorovinV #order
- An AC-Compatible Knuth-Bendix Order (KK, AV), pp. 47–59.
LICS-2003-KorovinV #order- Orienting Equalities with the Knuth-Bendix Order (KK, AV), p. 75–?.
ICALP-2001-KorovinV #constraints #theorem proving- Knuth-Bendix Constraint Solving Is NP-Complete (KK, AV), pp. 979–992.
- RTA-2001-KorovinV #order #using #verification
- Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order (KK, AV), pp. 137–153.
- LICS-2000-KorovinV #algebra
- A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering (KK, AV), pp. 291–302.
- RTA-1991-Bundgen #algorithm #simulation
- Simulation Buchberger’s Algorithm by Knuth-Bendix Completion (RB), pp. 386–397.
- ICALP-1990-Klop #term rewriting
- Term Rewriting Systems: From Church-Rosser to Knuth-Bendix and Beyond (JWK), pp. 350–369.
- ALP-1990-Steinbach #term rewriting
- AC-Termination of Rewrite Systems: A Modified Knuth-Bendix Ordering (JS), pp. 372–386.
- RTA-1989-Christian #performance #summary
- Fast Knuth-Bendix Completion: Summary (JC), pp. 551–555.
- ICALP-1987-Diekert #concurrent #on the #process
- On the Knuth-Bendix Completion for Concurrent Processes (VD), pp. 42–53.
- RTA-1987-Martin #how
- How to Choose Weights in the Knuth Bendix Ordering (UM), pp. 42–53.
- ICALP-1986-HermannP #algorithm #on the
- On Nontermination of Knuth-Bendix Algorithm (MH, IP), pp. 146–156.
- CADE-1986-Plaisted
- A Simple Non-Termination Test for the Knuth-Bendix Method (DAP), pp. 79–88.
- CADE-1984-Stickel #case study #commutative #proving #theorem proving
- A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering That x³=x Implies Ring Commutativity (MES), pp. 248–258.
