Sarah Winkler and Aart Middeldorp
Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 108, pp. 30:1 – 30:18, 2018.
pdf 
doi:10.4230/LIPIcs.FSCD.2018.30
Abstract
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.
BibTex
@inproceedings{SWAM-FSCD18, author = "Sarah Winkler and Aart Middeldorp", title = "Completion for Logically Constrained Rewriting", booktitle = "Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)", editor = "H{\'e}l{\`e}ne Kirchner", series = "Leibniz International Proceedings in Informatics" volume = 108, pages = "30:1--30:18", year = 2018, doi = "10.4230/LIPIcs.FSCD.2018.30"}