Paper: Context Matching for Compressed Terms (at LICS 2008)

Authors: Adria Gascón Guillem Godoy Manfred Schmidt-Schauß

Abstract

This paper is an investigation of the matching problem for term equations s = t where s contains context variables and first-order variables, and both terms s and t are given using some kind of compressed representation. The main result is a polynomial time algorithm for context matching with dags, when the number of different context variables is fixed for the problem. NP-completeness is obtained when the terms are represented using the more general formalism of singleton tree grammars. As an ingredient of this proof, we also show that the special case of first-order matching with singleton tree grammars is decidable in polynomial time.

BibTeX

  @InProceedings{GascnGodoySchmidtSc-ContextMatchingforC,
    author = 	 {Adria Gascón and Guillem Godoy and Manfred Schmidt-Schauß},
    title = 	 {Context Matching for Compressed Terms},
    booktitle =  {Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS 2008)},
    year =	 {2008},
    month =	 {June}, 
    pages =      {93--102},
    location =   {Pittsburgh, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }