Building and Combining Matching Algorithms

Christophe Ringeissen (1)

1 PESTO - Proof techniques for security protocols

The concept of matching is ubiquitous in declarative programming and in automated reasoning. For instance, it is a key mechanism to run rule-based programs and to simplify clauses generated by theorem provers. A matching problem can be seen as a particular conjunction of equations where each equation has a ground side. We give an overview of techniques that can be applied to build and combine matching algorithms. First, we survey mutation-based techniques as a way to build a generic matching algorithm for a large class of equational theories. Second, combination techniques are introduced to get combined matching algorithms for disjoint unions of theories. Then we show how these combination algorithms can be extended to handle non-disjoint unions of theories sharing only constructors. These extensions are possible if an appropriate notion of normal form is computable.

Mots clés: Matching; Unification; Combination of Theories; Syntactic Theories

Domaines: Logique en informatique [cs.LO]

Christophe Ringeissen. Building and Combining Matching Algorithms. Carsten Lutz; Uli Sattler; Cesare Tinelli; Anni-Yasmin Turhan; Frank Wolter. Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, 11560, Springer, pp.523-541, 2019, Lecture Notes in Computer Science, ⟨10.1007/978-3-030-22102-7_24⟩. ⟨hal-02187244⟩