Abstract

Completion is the process of turning a set of equations into an equivalent confluent and terminating set of rewrite rules. It is known that completion will always succeed if the input equations are ground and the employed reduction order is total on (equivalent) ground terms. Moreover, every reduced ground rewrite system can be obtained by completion from any equivalent set of ground equations. We present the first formalized correctness proofs of these results.

BibTeX

@inproceedings{AMCS-IWC17,
  author    = "Aart Middeldorp and Christian Sternagel",
  title     = "Formalized Ground Completion",
  booktitle = "Proceedings of the 6th International Workshop on Confluence
               (IWC 2017)",
  editor    = "Beniamino Accattoli and Bertram Felgenhauer",
  pages     = "51--55",
  year      = 2017
}