Skip to Main content Skip to Navigation
Book sections

Building and Combining Matching Algorithms

Christophe Ringeissen 1 
1 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : 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.
Document type :
Book sections
Complete list of metadata

Cited literature [53 references]  Display  Hide  Download
Contributor : Christophe Ringeissen Connect in order to contact the contributor
Submitted on : Wednesday, July 17, 2019 - 4:46:59 PM
Last modification on : Friday, February 4, 2022 - 3:29:53 AM


Files produced by the author(s)




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⟩



Record views


Files downloads