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