License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2022.8
URN: urn:nbn:de:0030-drops-162894
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16289/
Go to the corresponding LIPIcs Volume Portal

Ayala-Rincón, Mauricio ; Fernández, Maribel ; Silva, Gabriel Ferreira ; Sobrinho, Daniele Nantes

A Certified Algorithm for AC-Unification

pdf-format:
LIPIcs-FSCD-2022-8.pdf (0.9 MB)

Abstract

Implementing unification modulo Associativity and Commutativity (AC) axioms is crucial in rewrite-based programming and theorem provers. We modify Stickel’s seminal AC-unification algorithm to avoid mutual recursion and formalise it in the PVS proof assistant. More precisely, we prove the adjusted algorithm’s termination, soundness, and completeness. To do this, we adapted Fages' termination proof, providing a unique elaborated measure that guarantees termination of the modified AC-unification algorithm. This development (to the best of our knowledge) provides the first fully formalised AC-unification algorithm.

BibTeX - Entry

@InProceedings{ayalarincon_et_al:LIPIcs.FSCD.2022.8,
  author =	{Ayala-Rinc\'{o}n, Mauricio and Fern\'{a}ndez, Maribel and Silva, Gabriel Ferreira and Sobrinho, Daniele Nantes},
  title =	{{A Certified Algorithm for AC-Unification}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{8:1--8:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16289},
  URN =		{urn:nbn:de:0030-drops-162894},
  doi =		{10.4230/LIPIcs.FSCD.2022.8},
  annote =	{Keywords: AC-Unification, PVS, Certified Algorithms, Formal Methods, Interactive Theorem Proving}
}

Keywords: AC-Unification, PVS, Certified Algorithms, Formal Methods, Interactive Theorem Proving
Collection: 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Issue Date: 2022
Date of publication: 28.06.2022
Supplementary Material: Source code available through hyperlinks on the paper.

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