Slothrop: Knuth–Bendix completion with a modern termination checker. A Knuth-Bendix completion procedure is parametrized by a reduction ordering used to ensure termination of intermediate and resulting rewriting systems. While in principle any reduction ordering can be used, modern completion tools typically implement only Knuth-Bendix and path orderings. Consequently, the theories for which completion can possibly yield a decision procedure are limited to those that can be oriented with a single path order. In this paper, we present a variant on the Knuth-Bendix completion procedure in which no ordering is assumed. Instead we rely on a modern termination checker to verify termination of rewriting systems. The new method is correct if it terminates; the resulting rewrite system is convergent and equivalent to the input theory. Completions are also not just ground-convergent, but fully convergent. We present an implementation of the new procedure, Slothrop, which automatically obtains such completions for theories that do not admit path orderings.
Keywords for this software
References in zbMATH (referenced in 11 articles , 1 standard article )
Showing results 1 to 11 of 11.
- Winkler, Sarah; Middeldorp, Aart: Completion for logically constrained rewriting (2018)
- Sato, Haruhiko; Winkler, Sarah: Encoding dependency pair techniques and control strategies for maximal completion (2015)
- Bofill, Miquel; Rubio, Albert: Paramodulation with non-monotonic orderings and simplification (2013)
- Winkler, Sarah; Sato, Haruhiko; Middeldorp, Aart; Kurihara, Masahito: Multi-completion with termination tools (2013)
- Sternagel, Thomas; Zankl, Harald: KBCV -- Knuth-Bendix completion visualizer (2012)
- Winkler, Sarah; Middeldorp, Aart: AC completion with termination tools (2011)
- Nishida, Naoki; Sakai, Masahiko: Proving injectivity of functions via program inversion in term rewriting (2010)
- Winkler, Sarah; Sato, Haruhiko; Middeldorp, Aart; Kurihara, Masahito: Optimizing (\textmkb_\textTT) (2010)
- Nishida, Naoki; Sakai, Masahiko: Completion after program inversion of injective functions (2009)
- Sato, Haruhiko; Winkler, Sarah; Kurihara, Masahito; Middeldorp, Aart: Multi-completion with termination tools. (System description) (2008)
- Wehrman, Ian; Stump, Aaron; Westbrook, Edwin: Slothrop: Knuth-Bendix completion with a modern termination checker (2006)