bviousl , static ordering can onl  be non interleaving. The d  namic method is more e ible, since it can use more updated knowledge about variable bindings, but it also carries the largest runtime overhead, since it is invoked several times for each use of a rule bod .

The semi d  namic method is a compromise between the two  it is more powerful than the static method, because it can d namicall propose di erent orderings for di erent instances of the same rule  it also carnes less overhead than the d  namic method, because it is invoked onl  once for each use of a rule bod  .

The total time of proving a goal is the sum of the ordering time and the inference time.

Interleaving and d  namic methods have the best potential for reducing the inference time, but ma  significantl  augment the ordering time.   tatic methods do not devote time to ordering (it is done o  line), but have a limited potential for reducing the inference time.

The algorithms described in this paper can be used for all categories of ordering methods, alt hough in the e periments described in ection we have onl implemented semi d namic, non interleaving ordering methods  on each reduction, the rule bod  is ordered and added to the left end of the resolvent, and then the leftmost literal of the resolvent is selected for the ne t reduction step.

## 2.4 Related Work

The problem of computational ine cienc of logic inference was the sub ect of e tensive research. The most obvious aspect of this ine cienc is the possible non termination of everal researchers developed compile time and run time techni ues to detect a proof.

and avoid infinite computations ( e  chre e ecorte, 199 ).    certain success was achieved in providing more advanced control through emplo  ment of co routining for inter predicate s nchroni ation purposes ( lark c abe, 1979   orto, 19 Naish, 19 lso, infinite computations can be avoided b   pruning infinite branches that do not contain solutions (Vasak otter, 19 mith, enesereth, insberg, 19 ol, pt, Klop, s stem (  orris, 19 ) subgoals are automaticall  reordered to avoid 191). In the N  I nntermination.

till, even when the proof is finite, it is desirable to make it more e  cient.

eve ral researchers studied the problem of clause ordering ( mith, 19 9   ohen, 199 t io ni rponen, 199 ). If we are looking for 1991 aird, 199 o ne elle, 199 reiner all the solutions of a goal, then the e cienc does not depend on the clause order (assuming no cuts). Indeed, if some predicate has   clauses, and for some argument bindings these clauses produce all their solutions in times 1 2 m m then all solutions of the predicate under these bindings are obtained in time and 2 m, regardless of the order in which the clauses are applied. i erent clause orderings correspond to di erent orders in which branches are selected in a proof tree if we traverse the entire tree, then the number of traversal steps does not depend on the order of branch selection, though the order of solutions found does depend on it.

ubgoal ordering, as was demonstrated in ample 1, can significantl a ect the e cienc  of proving a goal. There are two ma or approaches to subgoal ordering. The first approach uses vanous heuristics to order subgoals, for e  ample hoose a subgoal whose predicate has the smallest number of matching clauses (   inker, 197 ).