Title
Combined Hierarchical Matching: the Regular Case
Document Type
Article
Digital Object Identifier (DOI)
10.4230/LIPIcs.FSCD.2022.6
Conference Title
7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Publication Date
2022
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.
Publisher Statement
© Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen;
Licensed under a Creative Commons License CC-BY 4.0.
Recommended Citation
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.
Comments
This article is openly accessible through the Dagstuhl Research Online Publication Server (DROPS) at: https://drops.dagstuhl.de/opus/volltexte/2022/16287/.