  We present the derivation reduction problem for SLD-resolution, the
undecidable problem of finding a finite subset of a set of clauses from which
the whole set can be derived using SLD-resolution. We study the reducibility of
various fragments of second-order Horn logic with particular applications in
Inductive Logic Programming. We also discuss how these results extend to
standard resolution.
