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.

Comments

This article is openly accessible through the Dagstuhl Research Online Publication Server (DROPS) at: https://drops.dagstuhl.de/opus/volltexte/2022/16287/.

Publisher Statement

© Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen;

Licensed under a Creative Commons License CC-BY 4.0.

Link to Full Text

Share

COinS