Context Trees

Abstract

Indexing data structures have a crucial impact on the performance of automated theorem provers. Examples are discrimination trees, which are like tries where terms are seen as strings and common prefixes are shared, and substitution trees, where terms keep their tree structure and all common contexts can be shared. Here we describe a new indexing data structure, called 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, where one also does not distinguish between internal and external variables. Experiments with matching benchmarks 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 significantly less than for other index structures.

The second and third author are partially supported by the Spanish CICYT project HEMOSS ref. TIC98-0949-C02-01. All test programs, implementations and benchmarks mentioned in this paper are available at www.lsi.upc.es/~roberto.