On the transformation of logic programs with instantiation based computation rules

AbstractWe give a formal description of a new transformation technique for declarative Horn clause programs. Our method allows the compilation of control information. We introduce the notion of an instantiation-based computation rule and present an algorithm to transform a given pair (ℙ, q), consisting of a Horn clause program P and a query pattern q for ℙ, into a new program ℙneu, which, for the given query pattern, will behave in the same way, under the standard computation rule of Prolog, as the original program ℙ behaves under a specified instantiation-based computation rule. We prove the soundness and completeness of the method and discuss its relation to existing techniques for the specification of control rules and the transformation of logic programs