Document Open Access Logo

A Certified Algorithm for AC-Unification

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

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.8.pdf
  • Filesize: 0.9 MB
  • 21 pages

Document Identifiers

Author Details

Mauricio Ayala-Rincón
  • Departments of Computer Science and Mathematics, University of Brasília, Brazil
Maribel Fernández
  • Department of Informatics, King’s College London, UK
Gabriel Ferreira Silva
  • Department of Computer Science, University of Brasília, Brazil
Daniele Nantes Sobrinho
  • Department of Computing, Imperial College London, UK
  • Department of Mathematics, University of Brasília, Brazil

Funding

Research supported by a FAP-DF (DE 00193.00001175/2021-11) and a CNPq (Universal 409003/2021-2) grant. First author partially funded by a CNPq productivity research grant 313290/2021-0. Fourth author partially funded by Edital DPI/DPG n. 03/2020.

Cite AsGet BibTex

Mauricio Ayala-Rincón, Maribel Fernández, Gabriel Ferreira Silva, and Daniele Nantes Sobrinho. A Certified Algorithm for AC-Unification. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 8:1-8:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.FSCD.2022.8

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Equational logic and rewriting
Keywords
  • AC-Unification
  • PVS
  • Certified Algorithms
  • Formal Methods
  • Interactive Theorem Proving

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

  • Source code available through hyperlinks on the paper.

References

  1. Mohamed Adi and Claude Kirchner. AC-Unification Race: The System Solving Approach, Implementation and Benchmarks. J. of Sym. Computation, 14(1):51-70, 1992. URL: https://doi.org/10.1016/0747-7171(92)90025-Y.
  2. Mauricio Ayala-Rincón, Washington de Carvalho Segundo, Maribel Fernández, Daniele Nantes-Sobrinho, and Ana Cristina Rocha Oliveira. A Formalisation of Nominal α-Equivalence with A, C, and AC Function Symbols. Theor. Comput. Sci., 781:3-23, 2019. URL: https://doi.org/10.1016/j.tcs.2019.02.020.
  3. Mauricio Ayala-Rincón, Washington de Carvalho Segundo, Maribel Fernández, Gabriel Ferreira Silva, and Daniele Nantes-Sobrinho. Formalising Nominal C-Unification Generalised with Protected Variables. Math. Struct. Comput. Sci., 31(3):286-311, 2021. URL: https://doi.org/10.1017/S0960129521000050.
  4. Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho. Nominal Narrowing. In 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, page 11. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.FSCD.2016.11.
  5. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. URL: https://doi.org/10.1017/CBO9781139172752.
  6. Dan Benanav, Deepak Kapur, and Paliath Narendran. Complexity of Matching Problems. J. of Sym. Computation, 3(1/2):203-216, 1987. URL: https://doi.org/10.1007/3-540-15976-2_22.
  7. Alexandre Boudet. Competing for the AC-Unification Race. J. of Autom. Reasoning, 11(2):185-212, 1993. URL: https://doi.org/10.1007/BF00881905.
  8. Alexandre Boudet, Evelyne Contejean, and Hervé Devie. A New AC Unification Algorithm with an Algorithm for Solving Systems of Diophantine Equations. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), pages 289-299. IEEE Computer Society, 1990. URL: https://doi.org/10.1109/LICS.1990.113755.
  9. James Cheney and Christian Urban. alpha-Prolog: A Logic Programming Language with Names, Binding and α-Equivalence. In Logic Programming, 20th International Conference, ICLP 2004, volume 3132 of LNCS, pages 269-283. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-27775-0_19.
  10. Michael Clausen and Albrecht Fortenbacher. Efficient Solution of Linear Diophantine Equations. J. of Sym. Computation, 8(1-2):201-216, 1989. URL: https://doi.org/10.1016/S0747-7171(89)80025-2.
  11. Evelyne Contejean. A Certified AC Matching Algorithm. In Rewriting Techniques and Applications, 15th International Conference, RTA 2004, Aachen, Germany, June 3-5, 2004, Proceedings, volume 3091 of LNCS, pages 70-84. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-25979-4_5.
  12. François Fages. Associative-Commutative Unification. In 7th International Conference on Automated Deduction, Napa, volume 170 of LNCS, pages 194-208. Springer, 1984. URL: https://doi.org/10.1007/978-0-387-34768-4_12.
  13. François Fages. Associative-Commutative Unification. J. of Sym. Computation, 3(3):257-275, 1987. URL: https://doi.org/10.1016/S0747-7171(87)80004-4.
  14. M. Fernández and M. J. Gabbay. Nominal Rewriting. Information and Computation, 205(6):917-965, 2007. URL: https://doi.org/10.1016/j.ic.2006.12.002.
  15. Jean-Pierre Jouannaud and Claude Kirchner. Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification. In Computational Logic - Essays in Honor of Alan Robinson, pages 257-321. The MIT Press, 1991. Google Scholar
  16. Deepak Kapur and Paliath Narendran. Double-exponential Complexity of Computing a Complete Set of AC-Unifiers. In Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), pages 11-21. IEEE Computer Society, 1992. URL: https://doi.org/10.1109/LICS.1992.185515.
  17. Florian Meßner, Julian Parsert, Jonas Schöpf, and Christian Sternagel. A Formally Verified Solver for Homogeneous Linear Diophantine Equations. In Interactive Theorem Proving - 9th International Conference, ITP 2018, volume 10895 of LNCS, pages 441-458. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94821-8_26.
  18. Sam Owre, John Rushby, and Natarajan Shankar. PVS: A Prototype Verification System. In Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, volume 607 of LNCS, pages 748-752. Springer, 1992. URL: https://doi.org/10.1007/3-540-55602-8_217.
  19. Sam Owre, Natarajan Shankar, John Rushby, and David Stringer-Calvert. PVS Language Reference. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA, 2000. URL: https://pvs.csl.sri.com/doc/pvs-language-reference.pdf.
  20. Andrew M Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, 2013. Google Scholar
  21. Mark E. Stickel. A Complete Unification Algorithm for Associative-Commutative Functions. In Advance Papers of the Fourth International Joint Conference on Artificial Intelligence, pages 71-76, 1975. URL: http://ijcai.org/Proceedings/75/Papers/011.pdf.
  22. Mark E. Stickel. A Unification Algorithm for Associative-Commutative Functions. J. of the ACM, 28(3):423-434, 1981. URL: https://doi.org/10.1145/322261.322262.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact