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"
}