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

https://hal.inria.fr/hal-02187244
Contributor : Christophe Ringeissen <>
Submitted on : Wednesday, July 17, 2019 - 4:46:59 PM
Last modification on : Friday, July 19, 2019 - 1:21:47 AM

File

survey-combi-matching.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

86

Files downloads

398