There are two main tasks that inductive logic programming (ILP) systems have to perform: refinement (of clauses and/or programs), and testing queries for logical implication (or nonimplication, in the case of negative examples). The authors introduce some transformations that can be used to modify queries, in order to yield more efficiently provable queries: the theta-, cut-, once-, and smartcall-transformations (to be precise, two of the transformations were proposed in earlier papers). While the theta-transformation is related to the construction of reduced clauses, the cut-transformation exploits the usage of the cut (!) in order to prune the search space. The once-transformation is a refinement of the cut-transformation, while the smartcall-transformation exploits derivations of the clause to be refined.

After introducing these four transformations, the authors show that all transformations can be implemented as algorithms that have a runtime that is polynomial in the length of the clause. They also prove that these transformations are sound, and yield more efficiently provable queries. The paper concludes by presenting the results of tests that have been performed.

The paper might be interesting for a better understanding of why the seemingly obvious transformations that are implemented in several ILP systems really yield improvisations. The paper is very readable, and clearly and formally written.