Advanced Indexing Operations on Substitution Trees

摘要

Indexing techniques support the retrieval and maintenance of large sets of terms. There is also an indexing method called substitution tree indexing that efficiently handles sets of substitutions. We present three advanced indexing operations for substitution trees: The multi-merge for the simultaneous unification of set of substitutions, the subsumption operation on two sets of substitutions, and the selection of 'lightest' substitutions of a set of substitutions. The indexing operations can be combined to obtain powerful reasoning tools for theorem provers.