Document Open Access Logo

Combined Hierarchical Matching: the Regular Case

Authors Serdar Erbatur , Andrew M. Marshall , Christophe Ringeissen

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.6.pdf
  • Filesize: 0.77 MB
  • 22 pages

Document Identifiers

Author Details

Serdar Erbatur
  • University of Texas at Dallas, TX, USA
Andrew M. Marshall
  • University of Mary Washington, Fredericksburg, VA, USA
Christophe Ringeissen
  • Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France

Acknowledgements

We would like to thank the reviewers for their comments that were very helpful to improve the readability of the paper.

Cite AsGet BibTex

Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Combined Hierarchical Matching: the Regular Case. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 6:1-6:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.FSCD.2022.6

Abstract

Matching algorithms are often central sub-routines in many areas of automated reasoning. They are used in areas such as functional programming, rule-based programming, automated theorem proving, and the symbolic analysis of security protocols. Matching is related to unification but provides a somewhat simplified problem. Thus, in some cases, we can obtain a matching algorithm even if the unification problem is undecidable. In this paper we consider a hierarchical approach to constructing matching algorithms. The hierarchical method has been successful for developing unification algorithms for theories defined over a constructor sub-theory. We show how the approach can be extended to matching problems which allows for the development, in a modular way, of hierarchical matching algorithms. Here we focus on regular theories, where both sides of each equational axiom have the same set of variables. We show that the combination of two hierarchical matching algorithms leads to a hierarchical matching algorithm for the union of regular theories sharing only a common constructor sub-theory.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Automated reasoning
Keywords
  • Matching
  • combination problem
  • equational theories

Metrics

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

References

  1. Alessandro Armando, Silvio Ranise, and Michaël Rusinowitch. A rewriting approach to satisfiability procedures. Inf. Comput., 183(2):140-164, 2003. Google Scholar
  2. Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge University Press, 1998. Google Scholar
  3. Franz Baader and Klaus U. Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. J. Symb. Comput., 21(2):211-243, 1996. Google Scholar
  4. Franz Baader and Wayne Snyder. Unification theory. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pages 445-532. Elsevier and MIT Press, 2001. Google Scholar
  5. Franz Baader and Cesare Tinelli. Combining decision procedures for positive theories sharing constructors. In Sophie Tison, editor, Rewriting Techniques and Applications, 13th International Conference, RTA 2002, Copenhagen, Denmark, July 22-24, 2002, Proceedings, volume 2378 of Lecture Notes in Computer Science, pages 352-366. Springer, 2002. Google Scholar
  6. Franz Baader and Cesare Tinelli. Deciding the word problem in the union of equational theories. Inf. Comput., 178(2):346-390, 2002. Google Scholar
  7. Leo Bachmair, Harald Ganzinger, Christopher Lynch, and Wayne Snyder. Basic paramodulation. Inf. Comput., 121(2):172-192, 1995. Google Scholar
  8. Bruno Blanchet. Modeling and verifying security protocols with the Applied Pi calculus and ProVerif. Foundations and Trends in Privacy and Security, 1(1-2):1-135, 2016. Google Scholar
  9. Peter Borovanský, Claude Kirchner, Hélène Kirchner, and Pierre-Etienne Moreau. ELAN from a rewriting logic point of view. Theor. Comput. Sci., 285(2):155-185, 2002. Google Scholar
  10. Alexandre Boudet and Evelyne Contejean. On n-syntactic equational theories. In Hélène Kirchner and Giorgio Levi, editors, Algebraic and Logic Programming, Third International Conference, Volterra, Italy, September 2-4, 1992, Proceedings, volume 632 of Lecture Notes in Computer Science, pages 446-457. Springer, 1992. Google Scholar
  11. Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn L. Talcott, editors. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of Lecture Notes in Computer Science. Springer, 2007. Google Scholar
  12. Eric Domenjoud, Francis Klay, and Christophe Ringeissen. Combination techniques for non-disjoint equational theories. In Alan Bundy, editor, Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994, Proceedings, volume 814 of Lecture Notes in Computer Science, pages 267-281. Springer, 1994. Google Scholar
  13. Ajay Kumar Eeralla, Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Rule-based unification in combined theories and the finite variant property. In Carlos Martín-Vide, Alexander Okhotin, and Dana Shapira, editors, Language and Automata Theory and Applications - 13th International Conference, LATA 2019, St. Petersburg, Russia, March 26-29, 2019, Proceedings, volume 11417 of Lecture Notes in Computer Science, pages 356-367. Springer, 2019. Google Scholar
  14. Serdar Erbatur, Deepak Kapur, Andrew M. Marshall, Paliath Narendran, and Christophe Ringeissen. Hierarchical combination. In Maria Paola Bonacina, editor, Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, volume 7898 of Lecture Notes in Computer Science, pages 249-266. Springer, 2013. Google Scholar
  15. Serdar Erbatur, Deepak Kapur, Andrew M. Marshall, Paliath Narendran, and Christophe Ringeissen. Unification and matching in hierarchical combinations of syntactic theories. In Carsten Lutz and Silvio Ranise, editors, Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015. Proceedings, volume 9322 of Lecture Notes in Computer Science, pages 291-306. Springer, 2015. Google Scholar
  16. Serdar Erbatur, Andrew M. Marshall, Deepak Kapur, and Paliath Narendran. Unification over distributive exponentiation (sub)theories. J. Autom. Lang. Comb., 16(2-4):109-140, 2011. Google Scholar
  17. Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Notions of knowledge in combinations of theories sharing constructors. In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 60-76. Springer, 2017. Google Scholar
  18. Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Terminating non-disjoint combined unification. In Maribel Fernández, editor, Logic-Based Program Synthesis and Transformation - 30th International Symposium, LOPSTR 2020, Bologna, Italy, September 7-9, 2020, Proceedings, volume 12561 of Lecture Notes in Computer Science, pages 113-130. Springer, 2020. Google Scholar
  19. Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Non-disjoint combined unification and closure by equational paramodulation. In Boris Konev and Giles Reger, editors, Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021, Birmingham, UK, September 8-10, 2021, Proceedings, volume 12941 of Lecture Notes in Computer Science, pages 25-42. Springer, 2021. Google Scholar
  20. Santiago Escobar, Catherine A. Meadows, and José Meseguer. Maude-NPA: Cryptographic protocol analysis modulo equational properties. In Alessandro Aldini, Gilles Barthe, and Roberto Gorrieri, editors, Foundations of Security Analysis and Design, Tutorial Lectures, volume 5705 of Lecture Notes in Computer Science, pages 1-50. Springer, 2007. Google Scholar
  21. Jean-Pierre Jouannaud and Hélène Kirchner. Completion of a set of rules modulo a set of equations. SIAM J. Comput., 15(4):1155-1194, 1986. Google Scholar
  22. Deepak Kapur, Paliath Narendran, and Lida Wang. An E-unification algorithm for analyzing protocols that use modular exponentiation. In Robert Nieuwenhuis, editor, Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Valencia, Spain, June 9-11, 2003, Proceedings, volume 2706 of Lecture Notes in Computer Science, pages 165-179. Springer, 2003. Google Scholar
  23. Claude Kirchner and Francis Klay. Syntactic theories and unification. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), Philadelphia, Pennsylvania, USA, June 4-7, 1990, pages 270-277. IEEE Computer Society, 1990. Google Scholar
  24. Catherine Meadows and Paliath Narendran. A unification algorithm for the group Diffie-Hellman protocol. In Informal Proceedings of the Workshop on Issues in the Theory of Security (WITS), 2002. Google Scholar
  25. Simon Meier, Benedikt Schmidt, Cas Cremers, and David A. Basin. The TAMARIN prover for the symbolic analysis of security protocols. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pages 696-701. Springer, 2013. Google Scholar
  26. Pierre-Etienne Moreau, Christophe Ringeissen, and Marian Vittek. A pattern matching compiler for multiple target languages. In Görel Hedin, editor, Compiler Construction, 12th International Conference, CC 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, volume 2622 of Lecture Notes in Computer Science, pages 61-76. Springer, 2003. Google Scholar
  27. Paliath Narendran. Solving linear equations over polynomial semirings. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, pages 466-472. IEEE Computer Society, 1996. Google Scholar
  28. Tobias Nipkow. Proof transformations for equational theories. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), Philadelphia, Pennsylvania, USA, June 4-7, 1990, pages 278-288. IEEE Computer Society, 1990. Google Scholar
  29. Tobias Nipkow. Combining matching algorithms: The regular case. J. Symb. Comput., 12(6):633-654, 1991. Google Scholar
  30. Christophe Ringeissen. Unification in a combination of equational theories with shared constants and its application to primal algebras. In Andrei Voronkov, editor, Logic Programming and Automated Reasoning, International Conference LPAR'92, St. Petersburg, Russia, July 15-20, 1992, Proceedings, volume 624 of Lecture Notes in Computer Science, pages 261-272. Springer, 1992. Google Scholar
  31. Christophe Ringeissen. Combining decision algorithms for matching in the union of disjoint equational theories. Inf. Comput., 126(2):144-160, 1996. Google Scholar
  32. Christophe Ringeissen. Matching in a class of combined non-disjoint theories. In Franz Baader, editor, Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings, volume 2741 of Lecture Notes in Computer Science, pages 212-227. Springer, 2003. Google Scholar
  33. Christophe Ringeissen. Building and combining matching algorithms. In Carsten Lutz, Uli Sattler, Cesare Tinelli, Anni-Yasmin Turhan, and Frank Wolter, editors, Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, volume 11560 of Lecture Notes in Computer Science, pages 523-541. Springer, 2019. Google Scholar
  34. Manfred Schmidt-Schauß. Unification in a combination of arbitrary disjoint equational theories. J. Symb. Comput., 8(1/2):51-99, 1989. Google Scholar
  35. Cesare Tinelli and Christophe Ringeissen. Unions of non-disjoint theories and combinations of satisfiability procedures. Theor. Comput. Sci., 290(1):291-353, 2003. 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 Imprint Privacy Contact