Logic in Computer Science (LICS 2000)

Paper: Approximate Pattern Matching is Expressible in Transitive Closure Logic (at LICS 2000)

Authors: Kjell Lemström Lauri Hella

Abstract

A sartorial query language facilitates the formulation of queries to a (string) database. One step towards an implementation of such a query language can be taken by defining a logical formalism expressing a known solution for the particular problem at hand. The simplicity of the logic is a desired property, because the simpler the logic that the query language is based on, the more efficiently it can be implemented. We introduce a logical formalism for expressing approximate pattern matching. The formalism uses properties of the dynamic programming approach; a minimizing path of a dynamic programming table is expressed by using a formula in an extension of first-order logic (FO). We consider the well-known problems of k mismatches and k differences. Assuming first that k is given as a part of the input, those problems are expressed by using deterministic transitive closure logic (FO(DTC)) and transitive closure logic (FO(TC)), respectively. We believe that in the general case the k differences is not expressible in FO(DTC), and show that solving this question in the affirmative is at least as hard as separating LOGSPACE from NLOGSPACE. We show, however, that if k is fixed, the k difference problem can be expressed by an FO(DTC) formula.

BibTeX

  @InProceedings{LemstrmHella-ApproximatePatternM,
    author = 	 {Kjell Lemström and Lauri Hella},
    title = 	 {Approximate Pattern Matching is Expressible in Transitive Closure Logic},
    booktitle =  {Proceedings of the Fifteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2000},
    year =	 2000,
    editor =	 {Martin Abadi},
    month =	 {June}, 
    pages =      {157--167},
    location =   {Santa Barbara, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }