based representation. owever, the large scale of such knowledge bases is likel to present significant e  cienc   problems to the inference engines.    sing automatic subgoal ordering techni ues, such as those described here, ma help to solve these problems.

The issue of subgoal ordering obtains a new significance with the development of Induc tive ogic rogramming ( avrac     eroski, 199 uggggg stems using this approach, such as I (Quinlan - ameron ones, 199 ), tr to build correct programs as fast as possible, without considering the e  cienc  of the produced programs.

ombining the DAC algorithm with Inductive  ogic  rogramming and other techni ues for the s nthesis of logic programs (such as the deductive and the constructive approaches)
looks like a promising direction.

## Appendix A. Proof Of Lemma 8

In this appendi we present the proof of a lemma which was omitted from the main te t of the paper for reasons of compactness. efore we prove it we show two au iliar lemmas.

Le mma  9 2 be two ordered sequences of subgoals, and Let 1 and lies between the values    (  1)    and
(2)
(     1 2)
a set of subgoals. The value of A 1 Proof:

enote

cost ( 1 ) nsols( 1) cn ( 1) l l l cost ( 2 ) nsols(  2) cn( 2) 2 2 2 , A, A 1 A 1 cost( 1 nsols( 1 1,2  1, 2 2) l, 2 2) 1 ) 1) l, 2 l, 2 l, 2 l, 2 l, 2 ,, 2" 2 i l 2 l 2 l, 2 l, 2 l, 2 l, 2
1,2 alwa s lies between   1 and ore e  actl  , the point    1,2 divides the segment to 1).

2 (because fil and n12 are positive and sum 2 with ratio l

$$\left(\begin{array}{c c c}{{}}&{{1,2}}&{{}}&{{}}\\ {{}}&{{}}&{{}}&{{1}}\end{array}\right)\quad\left(\begin{array}{c c c}{{}}&{{}}&{{}}\\ {{}}&{{}}&{{2}}\end{array}\right)$$
$$\begin{array}{r l}{2}&{{}\quad\quad\quad1\,,2}\end{array}$$

l 2 l In other words, 1,2 is a weighted average of 1 and 2. Note that 1 is the amount of resources spent in the proof tree of 1, 1, 2 the resources spent in the tree of 2, and 12 is their sum. 0, the more time (relativel ) we dedicate to the proof of 1, the closer 1.2 is to 1. This conclusion can be generali ed to a larger number of components in a concatenation (the proof is b  induction)

cost(A1) cn(A1 A2 ...Ak) - cn(A1) l cost(A1 A2 ...Ak) nsols(A1) cost(A2) A cn(A2) i, + ...+ cost(A1 A2 ...Ak) nsols(A1 A2 ...Ak-1) · cost(Ak) AR 1 c n(Ak) A 1  ... A R - 1 cost(A1 A2 ...Ak)