License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2013.287
URN: urn:nbn:de:0030-drops-40685
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4068/
Go to the corresponding LIPIcs Volume Portal

Sternagel, Christian ; Thiemann, René

Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion

pdf-format:
21.pdf (0.5 MB)

Abstract

We present extensions of our Isabelle Formalization of Rewriting that cover two historically related concepts: the Knuth-Bendix order and the Knuth-Bendix completion procedure.

The former, besides being the first development of its kind in a proof assistant, is based on a generalized version of the Knuth-Bendix order. We compare our version to variants from the literature and show all properties required to certify termination proofs of TRSs.

The latter comprises the formalization of important facts that are related to completion, like Birkhoff's theorem, the critical pair theorem, and a soundness proof of completion, showing that the strict encompassment condition is superfluous for finite runs. As a result, we are able to certify completion proofs.

BibTeX - Entry

@InProceedings{sternagel_et_al:LIPIcs:2013:4068,
  author =	{Christian Sternagel and Ren{\'e} Thiemann},
  title =	{{Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{287--302},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{Femke van Raamsdonk},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4068},
  URN =		{urn:nbn:de:0030-drops-40685},
  doi =		{10.4230/LIPIcs.RTA.2013.287},
  annote =	{Keywords: certification, completion, confluence, termination}
}

Keywords: certification, completion, confluence, termination
Collection: 24th International Conference on Rewriting Techniques and Applications (RTA 2013)
Issue Date: 2013
Date of publication: 24.06.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI