cl-banner

Completion for Logically Constrained Rewriting

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.

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.

 

  PDF |    doi:10.4230/LIPIcs.FSCD.2018.30  

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"
}
Nach oben scrollen