Document Open Access Logo

An Isabelle/HOL Formalization of Narrowing and Multiset Narrowing for E-Unifiability, Reachability and Infeasibility

Author Dohan Kim

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.24.pdf
  • Filesize: 0.9 MB
  • 19 pages

Document Identifiers

Author Details

Dohan Kim
  • Department of Computer Science, University of Innsbruck, Austria

Funding

Austrian Science Fund (FWF) project I5943.

Acknowledgements

The author would like to thank René Thiemann for his valuable comments and discussion on narrowing with special encoding and multiset narrowing.

Cite As Get BibTex

Dohan Kim. An Isabelle/HOL Formalization of Narrowing and Multiset Narrowing for E-Unifiability, Reachability and Infeasibility. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.ITP.2024.24

Abstract

We present an Isabelle/HOL formalization of narrowing for E-unifiability, reachability, and infeasibility. Given a semi-complete rewrite system ℛ and two terms s and t, we show a formalized proof that if narrowing terminates, then it provides a decision procedure for ℛ-unifiability for s and t, where ℛ is viewed as a set of equations. Furthermore, we present multiset narrowing and its formalization for multiset reachability and reachability analysis, providing decision procedures using certain restricted conditions on multiset reachability and reachability problems. Our multiset narrowing also provides a complete method for E-unifiability problems consisting of multiple goals if E can be represented by a complete rewrite system.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Equational logic and rewriting
Keywords
  • Narrowing
  • Multiset Narrowing
  • Unifiability
  • Reachability

Metrics

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

References

  1. An Isabelle/HOL Formalization of Rewriting for Certified Tool Assertions. Computational Logic group at the University of Innsbruck, URL: http://cl-informatik.uibk.ac.at/isafor/.
  2. Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho. Nominal narrowing. In Delia Kesner and Brigitte Pientka, editors, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal, volume 52 of LIPIcs, pages 11:1-11:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPICS.FSCD.2016.11.
  3. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, Cambridge, UK, 1998. Google Scholar
  4. Franz Baader and Wayne Snyder. Unification Theory. In Handbook of Automated Reasoning, Volume I, chapter 8, pages 445-532. Elsevier, Amsterdam, 2001. Google Scholar
  5. Clemens Ballarin. Tutorial to Locales and Locale Interpretation. URL: http:// isabelle.in.tum.de/doc/locales.pdf.
  6. Alexander Bockmayr. Contributions to the Theory of Logic-Functional Programming. PhD thesis, Fakultät für Informatik, Universität Karlsruhe, 1990. Google Scholar
  7. Andrew Cholewa, Santiago Escobar, and José Meseguer. Constrained narrowing for conditional equational theories modulo axioms. Sci. Comput. Program., 112:24-57, 2015. URL: https://doi.org/10.1016/J.SCICO.2015.06.001.
  8. Hubert Comon and Claude Kirchner. Constraint Solving on Terms. In Gerhard Goos, Juris Hartmanis, Jan van Leeuwen, Hubert Comon, Claude Marché, and Ralf Treinen, editors, Constraints in Computational Logics: Theory and Applications International Summer School, CCL '99 Gif-sur-Yvette, France, September 5-8, 1999 Revised Lectures, pages 47-103. Springer Berlin Heidelberg, Berlin, Heidelberg, 2001. URL: https://doi.org/10.1007/3-540-45406-3_2.
  9. Hubert Comon-Lundh and Stéphanie Delaune. The Finite Variant Property: How to Get Rid of Some Algebraic Properties. In Jürgen Giesl, editor, Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings, volume 3467 of Lecture Notes in Computer Science, pages 294-307. Springer, 2005. URL: https://doi.org/10.1007/978-3-540-32033-3_22.
  10. Nachum Dershowitz and David A. Plaisted. Rewriting. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pages 535-610. Elsevier and MIT Press, 2001. Google Scholar
  11. Francisco Durán, Steven Eker, Santiago Escobar, Narciso Martí-Oliet, José Meseguer, Rubén Rubio, and Carolyn L. Talcott. Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description). In Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, editors, Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, volume 13385 of Lecture Notes in Computer Science, pages 529-540. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-10769-6_31.
  12. Santiago Escobar, Ralf Sasse, and José Meseguer. Folding Variant Narrowing and Optimal Variant Termination. In Peter Csaba Ölveczky, editor, Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Paphos, Cyprus, March 20-21, 2010, Revised Selected Papers, volume 6381 of Lecture Notes in Computer Science, pages 52-68. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-16310-4_5.
  13. M. Fay. First-Order Unification in Equational Theories. In Fourth International Workshopon Automated Deduction, Austin, Texas, Proceedings, pages 161-167, 1979. Google Scholar
  14. Guillaume Feuillade, Thomas Genet, and Valérie Viet Triem Tong. Reachability Analysis over Term Rewriting Systems. J. Autom. Reason., 33(3-4):341-383, 2004. URL: https://doi.org/10.1007/S10817-004-6246-0.
  15. Jean H Gallier and Wayne Snyder. Complete sets of transformations for general E-unification. Theoretical Computer Science, 67(2-3):203-260, 1989. URL: https://doi.org/10.1016/0304-3975(89)90004-2.
  16. Michael Hanus. CHR(Curry): Interpretation and Compilation of Constraint Handling Rules in Curry. In Enrico Pontelli and Tran Cao Son, editors, Practical Aspects of Declarative Languages - 17th International Symposium, PADL 2015, Portland, OR, USA, June 18-19, 2015. Proceedings, volume 9131 of Lecture Notes in Computer Science, pages 74-89. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-19686-2_6.
  17. Nao Hirokawa, Aart Middeldorp, and Christian Sternagel. A New and Formalized Proof of Abstract Completion. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558 of Lecture Notes in Computer Science, pages 292-307. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_19.
  18. Jean-Marie Hullot. Canonical forms and unification. In Wolfgang Bibel and Robert A. Kowalski, editors, 5th Conference on Automated Deduction, Les Arcs, France, July 8-11, 1980, Proceedings, volume 87 of Lecture Notes in Computer Science, pages 318-334. Springer, 1980. URL: https://doi.org/10.1007/3-540-10009-1_25.
  19. Hélène Kirchner. On the Use of Constraints in Automated Deduction. In Andreas Podelski, editor, Constraint Programming: Basics and Trends, Châtillon Spring School, Châtillon-sur-Seine, France, May 16 - 20, 1994, Selected Papers, volume 910 of Lecture Notes in Computer Science, pages 128-146. Springer, 1994. URL: https://doi.org/10.1007/3-540-59155-9_8.
  20. John W. Lloyd. Foundations of Logic Programming, 3rd Edition. Springer, 2012. Google Scholar
  21. Salvador Lucas and Raúl Gutiérrez. Use of logical models for proving infeasibility in term rewriting. Inf. Process. Lett., 136:90-95, 2018. URL: https://doi.org/10.1016/J.IPL.2018.04.002.
  22. José Meseguer and Prasanna Thati. Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. High. Order Symb. Comput., 20(1-2):123-160, 2007. URL: https://doi.org/10.1007/S10990-007-9000-6.
  23. Aart Middeldorp and Erik Hamoen. Completeness results for basic narrowing. Appl. Algebra Eng. Commun. Comput., 5:213-253, 1994. URL: https://doi.org/10.1007/BF01190830.
  24. Aart Middeldorp, Satoshi Okui, and Tetsuo Ida. Lazy Narrowing: Strong Completeness and Eager Variable Elimination. Theor. Comput. Sci., 167(1&2):95-130, 1996. URL: https://doi.org/10.1016/0304-3975(96)00071-0.
  25. Robert Nieuwenhuis. Decidability and Complexity Analysis by Basic Paramodulation. Inf. Comput., 147(1):1-21, 1998. URL: https://doi.org/10.1006/INCO.1998.2730.
  26. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. Google Scholar
  27. Christian Sternagel and Akihisa Yamada. Reachability Analysis for Termination and Confluence of Rewriting. In Tomás Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I, volume 11427 of Lecture Notes in Computer Science, pages 262-278. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17462-0_15.
  28. Prasanna Thati and José Meseguer. Complete Symbolic Reachability Analysis Using Back-and-Forth Narrowing. In José Luiz Fiadeiro, Neil Harman, Markus Roggenbach, and Jan J. M. M. Rutten, editors, Algebra and Coalgebra in Computer Science: First International Conference, CALCO 2005, Swansea, UK, September 3-6, 2005, Proceedings, volume 3629 of Lecture Notes in Computer Science, pages 379-394. Springer, 2005. URL: https://doi.org/10.1007/11548133_24.
  29. Emanuele Viola. E-unifiability via Narrowing. In Antonio Restivo, Simona Ronchi Della Rocca, and Luca Roversi, editors, Theoretical Computer Science, 7th Italian Conference, ICTCS 2001, Torino, Italy, October 4-6, 2001, Proceedings, volume 2202 of Lecture Notes in Computer Science, pages 426-438. Springer, 2001. URL: https://doi.org/10.1007/3-540-45446-2_27.
  30. Akihiro Yamamoto. Completeness of extended unification based on basic narrowing. In Koichi Furukawa, Hozumi Tanaka, and Tetsunosuke Fujisaki, editors, Logic Programming '88, pages 1-10, Berlin, Heidelberg, 1989. Springer Berlin Heidelberg. Google Scholar
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 About DROPS Imprint Privacy Contact