On the transformation of logic programs with instantiation based computation rules (Q1119029)

A formal description of a new transformation technique for declarative Horn clause programs is presented. The aim of the paper is to solve the following problems: Being given a set P of Horn clauses and a query pattern q representing a set of queries, derive a computing rule based solely on the instantiation patterns of the goal statements which can occur during the execution of P for queries in the set defined by q and respectively, transforme P into a program whose trace, under the standard comutation rule, for queries of type q is equivalent to the trace of P under the derived computation rule. A formal and algorithmic approach and also the correctness of its solution for the case that the derived computation rule is a finite, well defined, complete uniquely representing and consistent instantiation-based computation rule for the given program and query pattern are developed. Some comments concerning the proposed method compared to some existing techniques for the specification of control rules and the transformation of programs are supplied in the last part of the paper.