Handbook of Automated Reasoning

9 Code trees

Code trees were introduced in [Voronkov 1994, Voronkov 1995]. A code tree is an index consisting of pieces of code instead of strings. Every piece of code is an instruction of an abstract machine able to perform the retrieval operation.

The general scheme of this indexing technique is as follows. Suppose that we have a retrieval condition R. For every indexed term l, we compile l into a sequence of instructions $i_1,\dots ,i_n$ of the abstract machine. This sequence represents a function I _l such that for every possible query term t we have $I_l\left(t\right)\iff R\left(l,t\right)$ . The sequence of instructions may, ...