Click on the title to obtain a gzip-ed PostScript version of the paper (86K).
Unification factoring seeks to rectify this omission by regarding the indexing and unification phases of clause resolution as a single process. This paper formalizes that process through the construction of factoring automata. A polynomial-time algorithm is given for constructing optimal factoring automata which preserve the clause selection strategy of Prolog. More generally, when the clause selection strategy is not fixed, constructing such an optimal automaton is shown to be NP-complete, solving an open trie minimization problem.
Unification factoring is implemented through a source code transformation that preserves the full semantics of Prolog. This transformation is specified in the paper, and using it, several well-known programs show performance improvements of up to 100% across three different systems.