Formalized Ground Completion

Aart Middeldorp and Christian Sternagel

Proceedings of the 6th International Workshop on Confluence (IWC 2017),   pp. 51 – 55, 2017.


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.




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