Hilfe Wegweiser Impressum Kontakt Einloggen





Context trees


Ganzinger,  Harald
Programming Logics, MPI for Informatics, Max Planck Society;

Nieuwenhuis,  Robert
Programming Logics, MPI for Informatics, Max Planck Society;

Nivela,  Pilar
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar

Ganzinger, H., Nieuwenhuis, R., & Nivela, P. (2001). Context trees. In R. Goré, A. Leitsch, & T. Nipkow (Eds.), Automated reasoning: First International Joint Conference, IJCAR 2001 (pp. 242-256). Berlin, Germany: Springer.

Indexing data structures are well-known to be crucial for the efficiency of the current state-of-the-art theorem provers. Examples are \emph{discrimination trees}, which are like tries where terms are seen as strings and common prefixes are shared, and \emph{substitution trees}, where terms keep their tree structure and all common \emph{contexts} can be shared. Here we describe a new indexing data structure, \emph{context trees}, where, by means of a limited kind of context variables, also common subterms can be shared, even if they occur below different function symbols. Apart from introducing the concept, we also provide evidence for its practical value. We describe an implementation of context trees based on Curry terms and on an extension of substitution trees with equality constraints and where one does not distinguish between \emph{internal} and \emph{external} variables. Experiments with matching show that our preliminary implementation is already competitive with tightly coded current state-of-the-art implementations of the other main techniques. In particular space consumption of context trees is substantially less than for other index structures.