Normalized Completion Revisited

Sarah Winkler and Aart Middeldorp

Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013), Leibniz International Proceedings in Informatics 21, pp. 319 – 334, 2013.


Normalized completion (Marché 1996) is a widely applicable and efficient technique for completion modulo theories. If successful, a normalized completion procedure computes a rewrite system that allows to decide the validity problem using normalized rewriting. In this paper we consider a slightly simplified inference system for finite normalized completion runs. We prove correctness, show faithfulness of critical pair criteria in our setting, and propose a different notion of normalizing pairs. We then show how normalized completion procedures can benefit from AC-termination tools instead of relying on a fixed AC-compatible reduction order. We outline our implementation of this approach in the completion tool mkbtt and present experimental results, including new completions.


  PDF |    doi:10.4230/LIPIcs.RTA.2013319  |  ©  Creative Commons License – NC – ND


author = "Sarah Winkler and Aart Middeldorp",
title = "Normalized Completion Revisited",
booktitle = "Proceedings of the 24th International Conference on Rewriting
Techniques and Applications",
editor = "Femke van Raamsdonk",
series = "Leibniz International Proceedings in Informatics",
volume = 21,
pages = "319--334",
year = 2013,
doi = "10.4230/LIPIcs.RTA.2013319"
Nach oben scrollen