Completion for Logically Constrained Rewriting
Sarah Winkler, Aart Middeldorp · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2018
We propose an abstract completion procedure for logically constrained term rewrite systems (LCTRSs). This procedure can be instantiated to both standard Knuth-Bendix completion and ordered completion for LCTRSs, and we present a succinct and uniform correctness proof. A prototype implementation illustrates the viability of the new completion approach.