Click on the title to obtain a gzip-ed PostScript version of the paper (86K).

###
Abstract:

The efficiency of resolution-based logic programming languages, such
as Prolog, depends critically on selecting and executing sets of
applicable clause heads to resolve against subgoals. Traditional
approaches to this problem have focused on using indexing to determine
the smallest possible applicable set. Despite their usefulness, these
approaches ignore the non-determinism inherent in many programming
languages to the extent that they do not attempt to optimize execution
*after* the applicable set has been determined.
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.