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

@inproceedings{SWAM-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"
}