Combined Hierarchical Matching: the Regular Case
Digital Object Identifier (DOI)
7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
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.
© Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen;
Licensed under a Creative Commons License CC-BY 4.0.
Erbatur, Serdar, Andrew M. Marshall, and Christophe Ringeissen. 2022. “Combined Hierarchical Matching: The Regular Case.” In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), edited by Amy P. Felty, 228:6:1-6:22. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.FSCD.2022.6.