Abstract

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.

BibTeX Entry

@inproceedings{WM-RTA13,
 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"
}