1: \documentstyle[12pt]{article}

2: \textheight=9.10in

3: \textwidth=6.50in

4: \topmargin=-0.70in

5: \oddsidemargin=0.05in

6: \evensidemargin=0.05in

7: \marginparwidth=0.50in

8: 

9: %\parskip=0.06in

10: \parindent=0.3in

11: 

12: \renewcommand{\baselinestretch}{1.16}

13: 

14: \newtheorem{definition}{Definition}[section]

15: \newtheorem{example}{Example}[section]

16: \newtheorem{remark}{Remark}[section]

17: \newtheorem{lemma}{Lemma}[section]

18: \newtheorem{theorem}[lemma]{Theorem}

19: \newtheorem{corollary}[lemma]{Corollary}

20: \newtheorem{proposition}[lemma]{Proposition}

21: 

22: \newtheorem{optimization}{Optimization}

23: \newtheorem{fact}{Fact}

24: 

25: 

26: \begin{document}

27: 

28: \title{\Large \bf SLT-Resolution for the

29: Well-Founded Semantics}

30: 

31: \author{Yi-Dong Shen\thanks{Work completed during a visit at

32: Department of Computing Science, 

33: University of Alberta, Canada.}\\

34: {\small  Department of Computer Science,

35: Chongqing University, Chongqing 400044, P.R.China}\\

36: {\small Email: ydshen@cs.ualberta.ca}\\[.1in]

37: Li-Yan Yuan  and Jia-Huai You\\

38: {\small  Department of Computing Science, University of

39: Alberta, Edmonton, Alberta, Canada T6G 2H1}\\

40: {\small  Email: \{yuan, you\}@cs.ualberta.ca}}

41: 

42: \date{}

43: 

44: \maketitle

45:  

46: \begin{abstract} 

47: Global SLS-resolution and SLG-resolution are two representative

48: mechanisms for top-down evaluation of the well-founded

49: semantics of general logic programs. Global SLS-resolution

50: is linear for query evaluation but suffers from infinite loops and redundant

51: computations. In contrast, SLG-resolution resolves infinite 

52: loops and redundant computations by means of tabling, but it is not linear. 

53: The principal disadvantage of a non-linear approach is that it cannot 

54: be implemented using a simple, efficient stack-based memory structure 

55: nor can it be easily extended to handle some 

56: strictly sequential operators such as cuts in Prolog.

57: 

58: In this paper, we present a linear tabling method, called {\em SLT-resolution},

59: for top-down evaluation of the well-founded semantics.

60: SLT-resolution is a substantial extension of SLDNF-resolution with tabling.

61: Its main features include: (1) It resolves infinite loops and redundant computations 

62: while preserving the linearity. (2) It is terminating, and sound and complete w.r.t. 

63: the well-founded semantics for programs with the bounded-term-size property 

64: with non-floundering queries. Its time complexity is comparable with SLG-resolution and

65: polynomial for function-free logic programs. (3) Because of its linearity for query 

66: evaluation, SLT-resolution bridges the gap between the well-founded semantics

67: and standard Prolog implementation techniques. It can be implemented by an extension 

68: to any existing Prolog abstract machines such as WAM or ATOAM.\\[.1in]

69: {\bf Keywords:} Well-founded semantics, procedural semantics, linear tabling,

70: Global SLS-resolution, SLG-resolution, SLT-resolution.

71: \end{abstract} 

72:  

73: \section{Introduction}

74: 

75: The central component of existing logic programming systems is a refutation

76: procedure, which is based on the resolution rule created by Robinson \cite{Robinson65}.

77: The first such refutation procedure, called {\em SLD-resolution},

78: was introduced by Kowalski \cite{Kow74, EK76}, and further formalized

79: by Apt and Van Emden \cite{AV82}. SLD-resolution is only suitable for

80: positive logic programs, i.e. programs without negation.

81: Clark \cite{clark78} extended SLD-resolution to {\em SLDNF-resolution}

82: by introducing the {\em negation as finite failure rule}, which is used 

83: to infer negative information. SLDNF-resolution is suitable for 

84: general logic programs, by which a ground negative literal

85: $\neg A$ succeeds if $A$ finitely fails, and fails if $A$ succeeds.

86: 

87: As an operational/procedural semantics of logic programs, SLDNF-resolution has 

88: many advantages, among the most important of which is its {\em linearity}

89: of derivations. Let $G_0 \Rightarrow_{C_1, \theta_1} G_1 \Rightarrow$

90: $...  \Rightarrow_{C_i, \theta_i} G_i$ be a derivation 

91: with $G_0$ the top goal and $G_i$ the 

92: latest generated goal. A resolution is said to be 

93: {\em linear} for query evaluation if when

94: applying the most widely used {\em depth-first} search rule,

95: it makes the next derivation step either by expanding $G_i$ using

96: a program clause (or a tabled answer), which yields

97: $G_i \Rightarrow_{C_{i+1}, \theta_{i+1}} G_{i+1}$,

98: or by expanding $G_{i-1}$ via backtracking.\footnote{

99: The concept of ``linear'' here is different from the one

100: used for SL-resolution \cite{KK71}.} It is with such linearity

101: that SLDNF-resolution can be realized easily and 

102: efficiently using a simple stack-based memory structure

103: \cite{WAM83, ZHOU96}. This has been sufficiently demonstrated

104: by Prolog, the first and yet the most popular logic programming

105: language which implements SLDNF-resolution. 

106:  

107: However, SLDNF-resolution suffers from two

108: serious problems. One is that the declarative semantics it

109: relies on, i.e. the {\em completion of programs} \cite{clark78}, incurs some

110: anomalies (see \cite{Ld87, sheph88} 

111: for a detailed discussion); and

112: the other is that it may generate infinite loops and a large amount

113: of redundant sub-derivations \cite{BAK91, DD93, VL89}.

114: 

115: The first problem with SLDNF-resolution has been perfectly settled by the discovery

116: of the {\em well-founded semantics} \cite{VRS91}.\footnote{Some other

117: important semantics, such as the {\em stable model semantics} \cite{GL88},

118: are also proposed. However, for the purpose of query evaluation

119: the well-founded semantics seems to be the most natural and robust.} 

120: Two representative methods were then proposed for 

121: top-down evaluation of such a new semantics:

122: Global SLS-resolution \cite{Prz89,Ross92} 

123: and SLG-resolution \cite{CSW95,chen96}.

124: 

125: Global SLS-resolution is a direct extension

126: of SLDNF-resolution. It overcomes the semantic anomalies of SLDNF-resolution by

127: treating infinite derivations as {\em failed}

128: and infinite recursions through negation as {\em undefined}. 

129: Like SLDNF-resolution, it is linear for query evaluation. However, it

130: inherits from SLDNF-resolution the problem of infinite loops

131: and redundant computations. Therefore, as the authors themselves

132: pointed out, Global SLS-resolution can be considered as a theoretical

133: construct \cite{Prz89} and is not effective in general \cite{Ross92}. 

134: 

135: SLG-resolution (similarly, Tabulated SLS-resolution \cite{BD98})

136: is a tabling mechanism for top-down evaluation of the well-founded

137: semantics. The main idea of tabling is to store intermediate results

138: of relevant subgoals and then use them to solve variants of the subgoals

139: whenever needed. With tabling no variant subgoals will be recomputed by applying

140: the same set of program clauses, so infinite loops can be avoided and 

141: redundant computations be substantially reduced

142: \cite{BD98,chen96,TS86,VL89,war92}. Like all other existing

143: tabling mechanisms, SLG-resolution adopts the {\em solution-lookup mode}.

144: That is, all nodes in a search tree/forest are partitioned into two subsets, 

145: {\em solution} nodes and {\em lookup} nodes. Solution nodes produce child nodes 

146: only using program clauses, whereas lookup nodes produce child nodes only using answers

147: in the tables. As an illustration, consider the derivation

148: $p(X) \Rightarrow_{C_{p_1}, \theta_1} q(X) \Rightarrow_{C_{q_1}, \theta_2} p(Y)$. 

149: Assume that so far no answers of $p(X)$ have been derived (i.e., 

150: currently the table for $p(X)$ is empty).

151: Since $p(Y)$ is a variant of $p(X)$ and thus a lookup node, 

152: the next derivation step is to expand $p(X)$ against a program clause, 

153: instead of expanding the latest generated goal $p(Y)$.

154: Apparently, such kind of resolutions is not linear for query evaluation. 

155: As a result, SLG-resolution cannot be implemented using

156: a simple, efficient stack-based memory structure 

157: nor can it be easily extended to handle some 

158: strictly sequential operators such as cuts in Prolog because the

159: sequentiality of these operators fully depends 

160: on the linearity of derivations.\footnote{

161: It is well known that cuts are indispensable in

162: real world programming practices.} This has been evidenced

163: by the fact that XSB, the best known state-of-the-art tabling system that implements

164: SLG-resolution, disallows clauses like \\

165: \indent $\qquad p(.) \leftarrow ...,t(.),!,...$\\

166: because the tabled predicate $t$

167: occurs in the scope of a cut \cite{SSW94, SSW98, SSWFR98}.

168: 

169: One interesting question then arises: Can we have a {\em linear tabling} method

170: for top-down evaluation of the well-founded semantics of general logic programs, 

171: which resolves infinite loops and redundant computations (like SLG-resolution) 

172: without sacrificing the linearity of SLDNF-resolution (like Global SLS-resolution)? 

173: In this paper, we give a positive answer to this question by developing

174: a new tabling mechanism, called {\em SLT-resolution}. SLT-resolution is 

175: a substantial extension of SLDNF-resolution with tabling. Its main features 

176: are as follows. 

177: 

178: \begin{itemize}

179: \item

180: SLT-resolution is based on finite {\em SLT-trees}. The construction of 

181: SLT-trees can be viewed as that of SLDNF-trees with an enhancement of

182: some loop handling mechanisms. Consider again the derivation

183: $p(X) \Rightarrow_{C_{p_1}, \theta_1} q(X) \Rightarrow_{C_{q_1}, \theta_2} p(Y)$.

184: Note that the derivation has gone into a loop since the proof of $p(X)$ needs 

185: the proof of $p(Y)$, a variant of $p(X)$. By SLDNF- or Global SLS-resolution,

186: $P(Y)$ will be expanded using the same set of program clauses as $p(X)$.

187: Obviously, this will lead to an infinite loop of the form

188: $p(X) \Rightarrow_{C_{p_1}}...p(Y)\Rightarrow_{C_{p_1}}...p(Z)\Rightarrow_{C_{p_1}}...$

189: In contrast, SLT-resolution will break the loop by disallowing $p(Y)$ to use

190: the clause $C_{p_1}$ that has been used by $p(X)$. As a result, SLT-trees are 

191: guaranteed to be finite for programs with the bounded-term-size property.

192: 

193: \item

194: SLT-resolution makes use of tabling to reduce redundant computations,

195: but is linear for query evaluation. Unlike SLG-resolution and all other

196: existing top-down tabling methods, SLT-resolution does not distinguish

197: between solution and lookup nodes. All nodes will be expanded by 

198: applying existing answers in tables, followed by program clauses. 

199: For instance, in the above example derivation, since currently there is no 

200: tabled answer available to $p(Y)$, $p(Y)$ will be expanded using some program 

201: clauses. If no program clauses are available to $p(Y)$, SLT-resolution 

202: would move back to $q(X)$ (assume using a depth-first control strategy). 

203: This shows that SLT-resolution is linear for query evaluation.  

204: When SLT-resolution moves back to $p(X)$, all program clauses that have

205: been used by $p(Y)$ will no longer be used by $p(X)$. This avoids

206: redundant computations.

207: 

208: \item

209: SLT-resolution is terminating, and sound and complete w.r.t. the well-founded

210: semantics for any programs with the bounded-term-size property with non-floundering

211: queries. Moreover, its time complexity is comparable with SLG-resolution and

212: polynomial for function-free logic programs.

213: 

214: \item

215: Because of its linearity for query evaluation, SLT-resolution can be implemented

216: by an extension to any existing Prolog abstract machines such as WAM \cite{WAM83}

217: or ATOAM \cite{ZHOU96}. This differs significantly from non-linear resolutions

218: such as SLG-resolution since their derivations cannot be organized using

219: a stack-based memory structure, which is the key to the Prolog implementation.

220: 

221: \end{itemize}

222: 

223: 

224: \subsection{Notation and Terminology} 

225: 

226: We present our notation and review some standard terminology of

227: logic programs \cite{Ld87}.

228: 

229: Variables begin with a capital letter, and predicate, function 

230: and constant symbols with a lower case letter. Let $p$ be a predicate

231: symbol. By $p(\vec{X})$ we denote an atom with the list $\vec{X}$

232: of variables. Let $S=\{A_1,...,A_n\}$ be a set of atoms. 

233: By $\neg .S$ we denote the complement $\{\neg A_1,...,\neg A_n\}$ of $S$.

234: 

235: \begin{definition}

236: {\em

237: A {\em general logic program} (program for short) is a finite set

238: of (program) clauses of the form

239: 

240: $\qquad A\leftarrow L_1,..., L_n$

241: 

242: \noindent where $A$ is an atom and $L_i$s are literals. 

243: $A$ is called the {\em head} and $L_1,...,L_n$ is called the

244: {\em body} of the clause. If a program has no clause with negative

245: literals in its body, it is called a {\em positive} program.

246: }

247: \end{definition}

248: 

249: \begin{definition}[\cite{Ross92}]

250: {\em

251: Let $P$ be a program and $\bar{p}$, $\bar{f}$ and $\bar{c}$

252: be a predicate symbol, function symbol and constant symbol

253: respectively, none of which appears in $P$. The {\em augmented

254: program} $\bar{P}=P\cup \{\bar{p}(\bar{f}(\bar{c}))\}$.

255: }

256: \end{definition}

257: 

258: \begin{definition}

259: {\em

260: A {\em goal} is a headless clause

261: $\leftarrow L_1,..., L_n$ where each $L_i$ is called a {\em subgoal}.

262: When $n=0$, the ``$\leftarrow$'' symbol is omitted. A {\em computation

263: rule} (or {\em selection rule}) is a rule for selecting one subgoal from a goal.

264: }

265: \end{definition}

266: 

267: Let $G_j=\leftarrow L_1,..., L_i,..., L_n$ be a 

268: goal with $L_i$ a positive subgoal. Let $C_l=L\leftarrow F_1,...,F_m$ be 

269: a clause such that $L\theta = L_i\theta$ where $\theta$ is an mgu (i.e. 

270: most general unifier). The {\em resolvent} of $G_j$ and $C_l$ on $L_i$ is the goal

271: $G_k=\leftarrow (L_1,...,L_{i-1}, F_1,...,F_m, L_{i+1},..., L_n)\theta$.

272: In this case, we say that the proof of $G_j$ is reduced to the proof of $G_k$.

273: 

274: The initial goal, $G_0=\leftarrow L_1,..., L_n$, is called

275: a {\em top} goal. Without loss of generality, we shall assume throughout

276: the paper that a top goal consists only of one atom (i.e. $n=1$ and $L_1$

277: is a positive literal). Moreover, we assume that the same computation rule $R$ always 

278: selects subgoals at the same position in any goals. For instance,

279: if $L_i$ in the above goal $G_j$ is selected by $R$, then $F_1\theta$ in $G_k$

280: will be selected by $R$ since $L_i$ and $F_1\theta$ are at the same position

281: in their respective goals.  

282: 

283: \begin{definition}

284: {\em

285: Let $P$ be a program. The {\em Herbrand universe} of $P$ is the set

286: of ground terms that use the function symbols and constants in $P$.

287: (If there is no constant in $P$, then an arbitrary one is added.)

288: The {\em Herbrand base} of $P$ is the set of ground atoms formed

289: by predicates in $P$ whose arguments are in the Herbrand universe.

290: By $\exists (Q)$ and $\forall (Q)$ we denote respectively

291: the existential and universal closure of $Q$ over the Herbrand

292: universe.

293: }

294: \end{definition}

295:  

296: \begin{definition}

297: {\em

298: A {\em Herbrand instantiated clause} of a program $P$ is a ground

299: instance of some clause $C$ in $P$ that is obtained by replacing

300: all variables in $C$ with some terms in the Herbrand universe of $P$.

301: The {\em Herbrand instantiation} of $P$ is the set of all

302: Herbrand instantiated clauses of $P$. 

303: }

304: \end{definition}

305: 

306: \begin{definition}

307: {\em

308: Let $P$ be a program and $H_P$ its Herbrand base.

309: A {\em partial interpretation} $I$

310: of $P$ is a set $\{A_1,...,A_m,\neg B_1,...,\neg B_n\}$

311: such that $\{A_1,...,A_m,B_1,...,B_n\}\subseteq H_P$ and

312: $\{A_1,...,A_m\}\cap \{B_1,...,B_n\}=\emptyset$. We use

313: $I^+$ and $I^-$ to refer to $\{A_1,...,A_m\}$ and

314: $\{B_1,...,B_n\}$, respectively.

315: }

316: \end{definition}

317: 

318: \begin{definition}

319: {\em

320: By a {\em variant} of a literal $L$ we mean a literal $L'$ that is the same 

321: as $L$ up to variable renaming. (Note that $L$ is a variant of itself.)

322: }

323: \end{definition}

324: 

325: Finally, a substitution $\alpha$ is {\em more general than} a substitution

326: $\beta$ if there exists a substitution $\gamma$ such that

327: $\beta=\alpha\gamma$. Note that $\alpha$ is more general than

328: itself because $\alpha=\alpha\varepsilon$ where $\varepsilon$

329: is the identity substitution \cite{Ld87}.  

330:  

331: \section{The Well-Founded Semantics}

332: 

333: In this section we review the definition of the well-founded

334: semantics of logic programs. We also present a new constructive

335: definition of the greatest unfounded set of a program, which has

336: technical advantages for the proof of our results.

337: 

338: \begin{definition}[\cite{Ross92, VRS91}]

339: \label{unf-set}

340: {\em

341: Let $P$ be a program and $H_P$ its Herbrand base. Let $I$ be a

342: partial interpretation. $U\subseteq H_P$ is an {\em unfounded set of $P$

343: w.r.t. $I$} if each atom $A\in U$ satisfies the following condition: For

344: each Herbrand instantiated clause $C$ of $P$ whose head is $A$, at least 

345: one of the following holds:

346: \begin{enumerate}

347: \item

348: The complement of some literal in the body of $C$ is in $I$.

349: 

350: \item

351: Some positive literal in the body of $C$ is in $U$.

352: \end{enumerate}

353: The {\em greatest unfounded set} of $P$ w.r.t. $I$,

354: denoted $U_P(I)$, is the union of all sets that are unfounded

355: w.r.t. $I$.

356: }

357: \end{definition}

358: 

359: 

360: \begin{definition}[\cite{Ross92}]

361: \label{trans-ops1}

362: {\em

363: Define the following transformations:

364: \begin{itemize}

365: \item

366: $A\in T_P(I)$ if and only if there is a Herbrand instantiated clause of 

367: $P$, $A\leftarrow L_1,...,L_m$, such that all $L_i$ are in $I$. 

368: 

369: \item

370: $\bar T_P(I)=T_P(I)\cup I$.

371: 

372: \item

373: $M_P(I)=\bigcup_{k=1}^\infty {\bar T}_P^k(I)$, where 

374: $\bar T_P^1(I)=\bar T_P(I)$, and for any $i>1$

375: $\bar T_P^i(I)=\bar T_P(\bar T_P^{i-1}(I))$.

376: 

377: \item

378: $U_P(I)$ is the greatest unfounded set of $P$ w.r.t. $I$,

379: as in Definition \ref{unf-set}.

380: 

381: \item

382: $V_P(I)=M_P(I)\cup \neg . U_P(I)$.

383: 

384: \end{itemize}

385: }

386: \end{definition}

387: 

388: Since $T_P(I)$ derives only positive literals,

389: the following result is straightforward.

390: 

391: \begin{lemma}

392: \label{lem2-1}

393: $\neg A\in M_P(I)$ if and only if $\neg A\in I$.

394: \end{lemma}

395: 

396: \begin{definition}[\cite{Ross92, VRS91}]

397: \label{trans-ops2}

398: {\em

399: Let $\alpha$ and $\beta$ be countable ordinals. The 

400: partial interpretations $I_\alpha$ are

401: defined recursively by

402: \begin{enumerate}

403: \item

404: For limit ordinal $\alpha$, $I_\alpha=\bigcup_{\beta <\alpha} I_\beta$,

405: where $I_0=\emptyset$. 

406: 

407: \item

408: For successor ordinal $\alpha +1$, $I_{\alpha +1}=V_P(I_\alpha)$.

409: \end{enumerate}

410: }

411: \end{definition}

412: 

413: The transfinite sequence $I_\alpha$ is

414: monotonically increasing (i.e. $I_\beta \subseteq I_\alpha$ 

415: if $\beta\leq \alpha$), so there exists the first ordinal

416: $\delta$ such that $I_{\delta +1}=I_\delta$. This fixpoint

417: partial interpretation, denoted $WF(P)$, is called the 

418: {\em well-founded model} of $P$. Then for any $A\in H_P$,

419: $A$ is true if $A\in WF(P)$, false 

420: if $\neg A\in WF(P)$, and undefined otherwise. 

421: 

422: \begin{lemma}

423: \label{lem2-2}

424: For any $J\subseteq WF(P)$, $M_P(J)\subseteq WF(P)$ and

425: $\neg .U_P(J)\subseteq WF(P)$.

426: \end{lemma}

427: 

428: \noindent {\bf Proof:} Let $J\subseteq I_m$. Since $I_\alpha$ is

429: monotonically increasing, $M_P(J)\subseteq I_{m+1}\subseteq WF(P)$ and

430: $\neg .U_P(J)\subseteq I_{m+1}\subseteq WF(P)$. $\Box$

431: 

432: \vspace{4mm}

433: 

434: The following definition is adapted from \cite{Prz90}.

435:  

436: \begin{definition}

437: \label{p-i}

438: {\em

439: $P|I$ is obtained from the Herbrand instantiation $P_{H_P}$ of $P$ by

440: \begin{itemize}

441: \item 

442: first deleting all clauses with a literal in their bodies

443: whose complement is in $I$, 

444: 

445: \item

446: then deleting all negative literals in the remaining clauses.

447: \end{itemize}

448: }

449: \end{definition}

450: 

451: Clearly $P|I$ is a positive program. Note that for any partial

452: interpretation $I$, $M_P(I)$ is a partial interpretation 

453: that consists of $I$ and 

454: all ground atoms that are iteratively derivable from $P_{H_P}$

455: and $I$. We observe that the

456: greatest unfounded set $U_P(I)$ of $P$ w.r.t. $I$ can be

457: constructively defined based on $M_P(I)$ and $P|M_P(I)$.

458: 

459: \begin{definition}

460: \label{vp}

461: {\em

462: Define the following two transformations:

463: \begin{itemize}

464: \item

465: $ N_P(I)=H_P-\bigcup_{k=1}^\infty {\bar T}_{P|M_P(I)}^k (M_P(I))$.

466: \item 

467: $O_P(I)=\bigcup_{k=1}^\infty {\bar T}_{P|M_P(I)}^k (M_P(I))-M_P(I)$.

468: \end{itemize} 

469: }

470: \end{definition}

471: 

472: We will show that $N_P(I)=U_P(I)$ (see Theorem \ref{wfs-1}).

473: The following result is immediate.

474: 

475: \begin{lemma}

476: \label{lem2-3}

477: $M_P(I)^+$, $N_P(I)$ and $O_P(I)$ are mutually disjoint

478: and $H_P=M_P(I)^+\cup N_P(I)\cup O_P(I)$.

479: \end{lemma}

480: 

481: From Definitions \ref{p-i} and \ref{vp} it is easily seen that

482: $O_P(I)=\bigcup_{i=1}^\infty S_i$, which is generated iteratively 

483: as follows: First, for each $A\in S_1$ there must be

484: a Herbrand instantiated clause of $P$ of the form

485: \begin{equation}

486: A\leftarrow B_1,...,B_m,\neg D_1,...,\neg D_n \qquad\qquad

487: \qquad\qquad\label{equa1}

488: \end{equation}

489: where all $B_i$s and some $\neg D_j$s are in $M_P(I)$ and

490: for the remaining $\neg D_k$s (not empty; otherwise $A\in M_P(I)$) neither $D_k$ 

491: nor $\neg D_k$ is in $M_P(I)$. Note that the proof of $A$

492: can be reduced to the proof of $\neg D_k$s given $M_P(I)$.

493: Then for each $A\in S_2$ there must be a clause like (\ref{equa1})

494: above where no $D_j$ is in $M_P(I)$, some $B_i$s 

495: are in $M_P(I)$, and the remaining $B_k$s (not empty) are in 

496: $S_1$. Continuing such process of reduction, 

497: for each $A\in S_{l+1}$ with $l\geq 1$ there must be a clause like (\ref{equa1})

498: above where no $D_j$ is in $M_P(I)$, some $B_i$s 

499: are in $M_P(I)$, and the remaining $B_k$s (not empty) are in 

500: $\bigcup_{i=1}^l S_i$.

501: 

502: The following lemma shows a useful property of literals in $O_P(I)$.

503: 

504: \begin{lemma}

505: \label{lem2-4}

506: Given $M_P(I)$, the proof of any $A\in O_P(I)$ can be reduced to the proof

507: of a set of ground negative literals $\neg E_j$s where neither $E_j$ 

508: nor $\neg E_j$ is in $M_P(I)$.

509: \end{lemma}

510: 

511: \noindent {\bf Proof:} Let $O_P(I)=\bigcup_{i=1}^\infty S_i$. 

512: The lemma is proved by induction on $S_i$. Obviously,

513: it holds for each $A\in S_1$. As inductive hypothesis,

514: assume that the lemma holds for 

515: any $A\in S_i$ with $1\leq i\leq l$. We now prove that

516: it holds for each $A\in S_{l+1}$.

517: 

518: Let $A\in S_{l+1}$. For convenience of presentation, 

519: in clause (\ref{equa1}) above for $A$

520: let $\{B_1,...,B_f\}\subseteq M_P(I)$ $(f<m)$,

521: $\{B_{f+1},...,B_m\}\subseteq \bigcup_{i=1}^l S_i$, 

522: $\{\neg D_1,...,\neg D_e\}\subseteq M_P(I)$ $(e\leq n)$,

523: and for each $D_k\in \{D_{e+1},...,D_n\}$ neither $D_k$ 

524: nor $\neg D_k$ is in $M_P(I)$. By the inductive hypothesis

525: the proof of $B_{f+1},...,B_m$ can be reduced to the proof of

526: a set $NS=\{\neg N_1,...,\neg N_t\}$ of negative literals where 

527: neither $N_j$ nor $\neg N_j$ is in $M_P(I)$. So the proof of

528: $A$ can be reduced to the proof of $\{\neg N_1,...,\neg N_t,

529: \neg D_{e+1},...,\neg D_n\}$. $\Box$

530: 

531: \begin{theorem}

532: \label{wfs-1}

533: $N_P(I)=U_P(I)$. 

534: \end{theorem}

535: 

536: \noindent {\bf Proof:} Let $A\in N_P(I)$ and $A\leftarrow B_1,...,B_m,

537: \neg D_1,...,\neg D_n$ be a Herbrand instantiated clause of $P$ for $A$.

538: By Definition \ref{vp}, either some $\neg B_i$ or $D_j$ is in $M_P(I)$,

539: or (when $A\leftarrow B_1,...,B_m$ is in $P|M_P(I)$) there exists some $B_i$

540: such that neither $B_i\in M_P(I)^+$ nor $B_i\in O_P(I)$, i.e. $B_i\in N_P(I)$

541: (see Lemma \ref{lem2-3}). By Definition \ref{unf-set}, $N_P(I)$ is an 

542: unfounded set w.r.t. $I$, so $N_P(I)\subseteq U_P(I)$.

543: 

544: Assume, on the contrary, that there is an $A\in U_P(I)$ but $A\not\in N_P(I)$.  

545: Since $U_P(I)\cap M_P(I)^+=\emptyset$, $A\in O_P(I)$. So there exists

546: a Herbrand instantiated clause $C$ of $P$

547: 

548: $\quad A\leftarrow B_1,...,B_m,\neg D_1,...,\neg D_n$

549: 

550: \noindent such that $C$ does not satisfy point 1 of Definition \ref{unf-set}

551: (since $I\subseteq M_P(I)$) and 

552: 

553: $\quad A\leftarrow B_1,...,B_m$

554: 

555: \noindent is in $P|M_P(I)$ where each $B_i$ is either in $M_P(I)^+$

556: or in $O_P(I)$. Since $A\in U_P(I)$, by point 2 

557: of Definition \ref{unf-set} some $B_j\in U_P(I)$ and thus $B_j\in O_P(I)$.

558: 

559: Repeating the above process leads to an infinite chain: the proof

560: of $A$ needs the proof of $B_j^1$ that needs the proof of $B_j^2$, and so on,

561: where each $B_j^i\in O_P(I)$. Obviously, for no $B_j^i$ along the chain 

562: its proof can be reduced to a set of ground negative literals 

563: $\neg E_j$s where neither $E_j$ nor $\neg E_j$ is in $M_P(I)$. This

564: contradicts Lemma \ref{lem2-4}, so $U_P(I)\subseteq N_P(I)$.  $\Box$

565: 

566: \vspace{4mm}

567: 

568: Starting with $I=\emptyset$, we compute $M_P(I)$, followed by 

569: $O_P(I)$ and $N_P(I)$. By Lemma \ref{lem2-2} and Theorem \ref{wfs-1},

570: each $A\in M_P(I)^+$ (resp. $A\in N_P(I)$) is true (resp. false) 

571: under the well-founded semantics. $O_P(I)$ is a set of {\em temporarily 

572: undefined} ground literals whose truth values cannot be determined at 

573: this stage of transformations based on $I$. We then do iterative

574: computations by letting $I=M_P(I)\cup \neg .N_P(I)$ until we reach 

575: a fixpoint. This forms the basis on which our operational procedure is

576: designed for top-down computation of the well-founded semantics.

577: 

578: \section{SLT-Trees and SLT-Resolution}

579: 

580: In this section, we define SLT-trees and SLT-resolution.

581: Here ``SLT'' stands for ``{\em L}inear {\em T}abulated resolution using

582: a {\em S}election/computation rule.'' 

583: 

584: Recall the familiar notion of a {\em tree} for describing 

585: the search space of a top-down proof procedure. For convenience,

586: a node in such a tree is represented by $N_i:G_i$, where $N_i$ is the 

587: node name and $G_i$ is a goal labeling the node. Assume no two 

588: nodes have the same name. Therefore, we can refer to nodes by their names.

589:  

590: \begin{definition}[\cite{shen97} with slight modification] 

591: \label{alist} 

592: {\em 

593: An {\it ancestor list} $AL_A$ of pairs $(N_i, A_i)$,

594: where $N_i$ is a node name and $A_i$ is an atom, is 

595: associated with each subgoal $A$ in a tree, which 

596: is defined recursively as follows. 

597: \begin{enumerate} 

598: \item 

599: If $A$ is at the root, then $AL_A=\emptyset$ unless otherwise specified. 

600: 

601: \item

602: Let $A$ be at node $N_{i+1}$ and $N_i$ be its parent node. 

603: If $A$ is copied or instantiated from some subgoal $A'$ at $N_i$ then  

604: $AL_A=AL_{A'}$.

605: 

606: \item

607: Let $N_i:G_i$ be a node that contains a positive literal $B$. Let $A$ be 

608: at node $N_{i+1}$ that is obtained from $N_i$ by resolving $G_i$ against

609: a clause $B' \leftarrow L_1, ..., L_n$ on the literal $B$ with

610: an mgu $\theta$. If $A$ is $L_j \theta$ for some $1 \leq j \leq n$,

611: then $AL_A = \{(N_i,B)\} \cup AL_B$. 

612: \end{enumerate} 

613: } 

614: \end{definition} 

615: 

616: Apparently, for any subgoals $A$ and $B$ if $A$ is in the ancestor list

617: of $B$, i.e. $(\_,A) \in AL_B$, the proof of $A$ needs the proof of $B$.

618: Particularly, if $(\_,A) \in AL_B$ and $B$ is a variant of $A$, the derivation

619: goes into a loop. This leads to the following.

620: 

621: \begin{definition}

622: \label{loop-def}

623: {\em 

624: Let $R$ be a computation rule and 

625: $A_i$ and $A_k$ be two subgoals that are selected by $R$ at nodes $N_i$ and $N_k$, 

626: respectively. If $(N_i,A_i) \in AL_{A_k}$, $A_i$ (resp. $N_i$) is called an  

627: {\em ancestor subgoal} of $A_k$ (resp. {\em an ancestor node} of $N_k$).  

628: If $A_i$ is both an ancestor subgoal and a variant,

629: i.e. an {\em ancestor variant subgoal}, of $A_k$,

630: we say the derivation goes into a {\em loop}, where $N_k$ and

631: all its ancestor nodes involved in the loop are called {\em loop nodes}

632: and the clause used by $A_i$ to generate this loop

633: is called a {\em looping clause} of $A_k$ w.r.t. $A_i$. 

634: We say a node is {\em loop-dependent} if it is a loop node or an ancestor node

635: of some loop node. Nodes that are not loop-dependent are  

636: {\em loop-independent}.

637: } 

638: \end{definition}

639: 

640: In tabulated resolutions, intermediate positive and negative 

641: (or alternatively, undefined) answers of some subgoals will be stored 

642: in tables at some stages. Such answers are called {\em tabled answers}.

643: Let $TB_f$ be a table that stores some ground negative answers; i.e.  

644: for each $A\in TB_f$ $\neg A\in WF(P)$. In addition, we introduce a

645: special subgoal, $u^*$, which is assumed to occur in neither

646: programs nor top goals. $u^*$ will be used to substitute for

647: some ground negative subgoals whose truth values are 

648: temporarily undefined. We now define SLT-trees.

649: 

650: \begin{definition}[SLT-trees]

651: \label{slt-tree}

652: {\em

653: Let $P$ be a program, $G_0$ a top goal, and $R$ a computation rule.

654: Let $TB_f$ be a set of ground atoms such that for each $A\in TB_f$ $\neg A\in WF(P)$.

655: The {\em SLT-tree} $T_{G_0}$ for $(P \cup \{G_0\},TB_f)$ via $R$ is a tree 

656: rooted at node $N_0:G_0$ such that for any node $N_i:G_i$ in the tree

657: with $G_i=\leftarrow L_1,...,L_n$:

658: 

659: \begin{enumerate}

660: \item

661: If $n=0$ then $N_i$ is a {\em success} leaf, marked by $\Box_t$.

662: 

663: \item

664: If $L_1=u^*$ then $N_i$ is a {\em temporarily undefined} 

665: leaf, marked by $\Box_{u^*}$.

666: 

667: \item

668: Let $L_j$ be a positive literal selected by $R$. Let $C_{L_j}$ be the set

669: of clauses in $P$ whose heads unify with $L_j$ and $LC_{L_j}$ be the set of

670: looping clauses of $L_j$ w.r.t. its ancestor variant subgoals. If 

671: $C_{L_j}-LC_{L_j}=\emptyset$ then $N_i$ is a {\em failure} leaf, marked by $\Box_f$;

672: else the children of $N_i$ are obtained by resolving 

673: $G_i$ with each of the clauses in $C_{L_j}-LC_{L_j}$ over the literal $L_j$.

674: 

675: \item

676: Let $L_j=\neg A$ be a negative literal selected by $R$. If $A$ is not ground then

677: $N_i$ is a {\em flounder} leaf, marked by $\Box_{fl}$; else if 

678: $A$ is in $TB_f$ then $N_i$ has only one child that is labeled

679: by the goal $\leftarrow L_1,...,L_{j-1},L_{j+1},...,L_n$; else build an SLT-tree

680: $T_{\leftarrow A}$ for $(P \cup \{\leftarrow A\},TB_f)$ via $R$, where 

681: the subgoal $A$ at the root inherits the ancestor

682: list $AL_{L_j}$ of $L_j$. We consider the following cases:

683: 

684: \begin{enumerate}

685: \item

686: If $T_{\leftarrow A}$ has a success leaf then 

687: $N_i$ is a {\em failure} leaf, marked by $\Box_f$;

688: 

689: \item

690: If $T_{\leftarrow A}$ has no success leaf but a flounder leaf then

691: $N_i$ is a {\em flounder} leaf, marked by $\Box_{fl}$;

692: 

693: \item

694: Otherwise, $N_i$ has only one child that is labeled

695: by the goal $\leftarrow L_1,...,L_{j-1},L_{j+1},...,$ $L_n,u^*$ if $L_n\neq u^*$

696: or $\leftarrow L_1,...,L_{j-1},L_{j+1},...,L_n$ if $L_n= u^*$. 

697: \end{enumerate}

698: \end{enumerate} 

699: }

700: \end{definition}

701: 

702: In an SLT-tree, there may be four types of leaves: success leaves $\Box_t$,

703: failure leaves $\Box_f$, temporarily undefined 

704: leaves $\Box_{u^*}$, and flounder leaves $\Box_{fl}$. These leaves

705: respectively represent successful, failed, (temporarily) undefined,

706: and floundering derivations (see Definition \ref{branch}).

707: In this paper, we shall not discuss floundering $-$ a situation where

708: a non-ground negative literal is selected by a computation rule $R$

709: (see \cite{chan88, dra95, LAC99, Prz89-3} for discussion on such topic). Therefore,

710: in the sequel we assume that no SLT-trees contain flounder leaves.

711:  

712: The construction of SLT-trees can be viewed as that of SLDNF-trees 

713: \cite{clark78, Ld87}

714: enhanced with the following loop-handling mechanisms: (1) Loops are detected

715: using ancestor lists of subgoals. Positive loops occur within SLT-trees, whereas

716: negative loops (i.e. loops through negation) 

717: occur across SLT-trees (see point 4 of Definition \ref{slt-tree}, where the {\em child}

718: SLT-tree $T_{\leftarrow A}$ is connected to its parent SLT-tree by letting

719: $A$ at the root of $T_{\leftarrow A}$ inherit the ancestor

720: list $AL_{L_j}$ of $L_j$). (2) Loops are broken by disallowing

721: subgoals to use looping clauses for node expansion 

722: (see point 3 of Definition \ref{slt-tree}). 

723: This guarantees that SLT-trees are

724: finite (see Theorem \ref{tree-finite}). (3) Due to the exclusion of 

725: looping clauses, some answers may be missed in an SLT-tree. 

726: Therefore, for any ground negative

727: subgoal $\neg A$ its answer (true or false) can be definitely 

728: determined only when $A$ is given to be false (i.e. $A\in TB_f$) or

729: the proof of $A$ via the SLT-tree $T_{\leftarrow A}$ succeeds (i.e.

730: $T_{\leftarrow A}$ has a success leaf). Otherwise, $\neg A$ is assumed to be

731: temporarily undefined and is replaced by $u^*$ (see point 4 of Definition 

732: \ref{slt-tree}). Note that $u^*$ is only introduced to signify the existence

733: of subgoals whose truth values are temporarily undefined. Therefore, keeping

734: one $u^*$ in a goal is enough for such a purpose (see point 4 (c)). From 

735: point 2 of Definition \ref{slt-tree} we see that goals

736: with a subgoal $u^*$ cannot lead to a success leaf. However,

737: they may arrive at a failure leaf if one of the remaining subgoals fails.    

738:  

739: For convenience, we use dotted edges to connect parent and child

740: SLT-trees, so that negative loops can be clearly identified (see Figure \ref{fig2}).

741: Moreover, we refer to $T_{G_0}$, the {\em top} SLT-tree, 

742: along with all its descendant SLT-trees

743: as a {\em generalized} SLT-tree for $(P\cup \{G_0\},TB_f)$, denoted $GT_{P, G_0}$

744: (or simply $GT_{G_0}$ when no confusion would occur).

745: Therefore, a path of a generalized SLT-tree may come 

746: across several SLT-trees through dotted edges.

747: 

748: \begin{example}

749: \label{eg3-2}

750: {\em

751: Consider the following program and let $G_0=\leftarrow p(X)$ be the top goal.

752: \begin{tabbing} 

753: \hspace{.2in} $P_1$: \= $p(X) \leftarrow q(X).$ \`$C_{p_1}$ \\ 

754: \> $p(a).$ \`$C_{p_2}$ \\ 

755: \> $q(X) \leftarrow \neg r.$ \`$C_{q_1}$ \\ 

756: \> $q(X) \leftarrow w.$ \`$C_{q_2}$ \\ 

757: \> $q(X) \leftarrow p(X).$ \`$C_{q_3}$ \\ 

758: \> $r \leftarrow \neg s.$ \`$C_{r_1}$ \\ 

759: \> $s \leftarrow \neg r.$ \`$C_{s_1}$ \\ 

760: \> $w \leftarrow \neg w,v.$ \`$C_{w_1}$  

761: \end{tabbing} 

762: For convenience, let us choose the left-most computation rule and let $TB_f=\emptyset$. 

763: The generalized SLT-tree $GT_{\leftarrow p(X)}$

764: for $(P_1\cup \{\leftarrow p(X)\},\emptyset)$ is shown in Figure \ref{fig2},\footnote{

765: For simplicity, in depicting SLT-trees 

766: we omit the ``$\leftarrow$'' symbol in goals.} 

767: which consists of five SLT-trees that are rooted at $N_0$, $N_6$, $N_8$,

768: $N_{10}$ and $N_{16}$, respectively.

769: $N_2$ and $N_{15}$ are success leaves because they are labeled by an empty goal.

770: $N_{10}$, $N_{16}$ and $N_{17}$ are failure leaves because they have

771: no clauses to unify with except for the looping clauses $C_{r_1}$

772: (for $N_{10}$) and $C_{w_1}$ (for $N_{16}$). $N_{11}$, $N_{12}$ and

773: $N_{13}$ are temporarily undefined leaves because their goals consist only

774: of $u^*$. 

775: }

776: \end{example}

777: 

778: \begin{figure}[htb] 

779: \centering

780: 

781: \setlength{\unitlength}{3947sp}%

782: %

783: \begingroup\makeatletter\ifx\SetFigFont\undefined%

784: \gdef\SetFigFont#1#2#3#4#5{%

785:   \reset@font\fontsize{#1}{#2pt}%

786:   \fontfamily{#3}\fontseries{#4}\fontshape{#5}%

787:   \selectfont}%

788: \fi\endgroup%

789: \begin{picture}(4062,3321)(1051,-3286)

790: \thinlines

791: \put(3601,-561){\vector(-2,-1){380}}

792: \put(3901,-561){\vector( 2,-1){380}}

793: \put(3751,-561){\vector( 0,-1){200}}

794: \put(4351,-136){\vector(-2,-1){380}}

795: \put(4651,-136){\vector( 2,-1){380}}

796: \put(2621,-1226){\vector(-2,-1){0}}

797: \multiput(3001,-1036)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

798: \put(3751,-1036){\vector( 0,-1){200}}

799: \put(2476,-1486){\vector( 0,-1){200}}

800: \put(1946,-2126){\vector(-2,-1){0}}

801: \multiput(2326,-1936)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

802: \put(1876,-2386){\vector( 0,-1){200}}

803: \put(2026,-2836){\vector( 2,-1){380}}

804: \put(4726,-1036){\vector( 2,-1){380}}

805: \put(4051,-1486){\vector( 2,-1){380}}

806: \put(2551,-1936){\vector( 2,-1){380}}

807: \put(3151,-1036){\vector( 0,-1){200}}

808: \put(3371,-1676){\vector(-2,-1){0}}

809: \multiput(3751,-1486)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

810: \put(1421,-3026){\vector(-2,-1){0}}

811: \multiput(1801,-2836)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

812: \put(2776,-961){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_3:$ $\neg r$ }}}

813: \put(3451,-961){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_4:$ $w$ }}}

814: \put(4051,-961){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_5:$ $p(X)$ }}}

815: \put(3451,-736){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{q_2}$}}}

816: \put(4201,-661){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{q_3}$}}}

817: \put(4951,-211){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{p_2}$}}}

818: \put(3826,-211){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{p_1}$}}}

819: \put(3001,-661){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{q_1}$}}}

820: \put(3451,-511){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_1:$  $q(X)$}}}

821: \put(2251,-1411){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_6:$ $ r$ }}}

822: \put(3826,-1186){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{w_1}$}}}

823: \put(3451,-1411){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{14}:$ $\neg w,v$ }}}

824: \put(2551,-1636){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{r_1}$}}}

825: \put(2101,-1861){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_7:$ $\neg s$ }}}

826: \put(1651,-2311){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_8:$ $s$ }}}

827: \put(1951,-2536){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{s_1}$}}}

828: \put(1501,-2761){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_9:$ $\neg r$ }}}

829: \put(4126,-61){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_0:$ $p(X)$ }}}

830: \put(4951,-1111){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{p_2}$}}}

831: \put(3226,-1786){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

832: \put(3001,-1936){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{16}:$ $w$ }}}

833: \put(4051,-1936){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{17}:$ $v, u^*$ }}}

834: \put(1051,-3286){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{10}:$ $r$ }}}

835: \put(5026,-1486){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{15}:$}}}

836: \put(5101,-1336){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_t$}}}

837: \put(4426,-1786){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

838: \put(2926,-2236){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_{u^*}$ }}}

839: \put(2851,-2386){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{12}:$ $u^*$ }}}

840: \put(1276,-3136){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

841: \put(2401,-3136){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_{u^*}$ }}}

842: \put(2326,-3286){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{11}:$ $u^*$ }}}

843: \put(5026,-436){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_t$}}}

844: \put(5026,-586){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_2:$}}}

845: \put(2851,-1561){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{13}:$ $u^*$ }}}

846: \put(3076,-1411){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_{u^*}$ }}}

847: \end{picture}

848:  

849: \caption{The generalized SLT-tree $GT_{\leftarrow p(X)}$ for 

850: $(P_1\cup \{\leftarrow p(X)\},\emptyset)$.}\label{fig2}

851: \end{figure} 

852: 

853: SLT-trees have some nice properties. Before proving those properties,

854: we reproduce the definition of bounded-term-size programs.

855: The following definition is adapted from \cite{VG89}.

856: 

857: \begin{definition}

858: \label{bounded-term-size}

859: {\em

860: A program has the {\em bounded-term-size} property if there is a function

861: $f(n)$ such that whenever a top goal $G_0$ has no argument whose term size exceeds

862: $n$, then no subgoals and tabled answers in any generalized SLT-tree

863: $GT_{G_0}$ have an argument whose term size exceeds $f(n)$.

864: }

865: \end{definition} 

866: 

867: The following result shows that the construction of SLT-trees

868: is always terminating for programs with the bounded-term-size property.

869: 

870: \begin{theorem}

871: \label{tree-finite}

872: Let $P$ be a program with the bounded-term-size property, 

873: $G_0$ a top goal and $R$ a computation rule. The generalized SLT-tree

874: $GT_{G_0}$ for $(P \cup \{G_0\},TB_f)$ via $R$ is finite.

875: \end{theorem}

876: 

877: \noindent {\bf Proof:}

878: The bounded-term-size property guarantees that no term occurring

879: on any path of $GT_{G_0}$ can have size greater than

880: $f(n)$, where $n$ is a bound on the size of terms in the top goal $G_0$.

881: Assume, on the contrary, that $GT_{G_0}$

882: is infinite. Then it must have an infinite path because its branching factor

883: (i.e. the average number of children of all nodes in the tree)

884: is bounded by the finite number of clauses in $P$. Since $P$ has only a finite

885: number of predicate, function and constant symbols, some positive subgoal $A_0$

886: selected by $R$ must have infinitely many variant descendants 

887: $A_1,A_2,..., A_i,...$ on the path 

888: such that the proof of $A_0$ needs the proof of $A_1$ that needs the proof of 

889: $A_2$, and so on. That is, $A_i$ is an ancestor variant subgoal of $A_j$ for any

890: $0\leq i <j$. Let $P$ have totally $m$ clauses that can unify with $A_0$.

891: Then by point 3 of Definition \ref{slt-tree}, $A_m$, when selected by $R$, 

892: will have no clause to unify with except for the $m$ looping clauses. That is, $A_m$

893: shoud be at a leaf, contradicting that it has variant decendants on the path. $\Box$

894: 

895: \begin{definition}

896: \label{branch}

897: {\em

898: Let $T_{G_0}$ be the SLT-tree for $(P \cup \{G_0\},TB_f)$.

899: A {\em successful} (resp. {\em failed or undefined}) 

900: branch of $T_{G_0}$ is a branch that ends at a

901: success (resp. failure or temporarily undefined) leaf.

902: A {\em correct answer substitution} for $G_0$ is given by 

903: $\theta=\theta_1...\theta_n$ where the $\theta_i$s are the most

904: general unifiers used at each step along a successful 

905: branch of $T_{G_0}$. 

906: An {\em SLT-derivation} of $(P \cup \{G_0\},TB_f)$ is a branch of $T_{G_0}$. 

907: }

908: \end{definition}

909: 

910: Another principal property of SLT-trees is that

911: correct answer substitutions for top goals

912: are sound w.r.t. the well-founded semantics.

913: 

914: \begin{theorem}

915: \label{ans-subs}

916: Let $P$ be a program with the bounded-term-size property, 

917: $G_0=\leftarrow Q_0$ a top goal, and 

918: $T_{G_0}$ the SLT-tree for $(P\cup\{G_0\},TB_f)$.

919: For any correct answer substitution $\theta$ for $G_0$ in $T_{G_0}$  

920: $WF(P) \models \forall (Q_0\theta)$.

921: \end{theorem}

922: 

923: \noindent {\bf Proof:}

924: Let $d$ be the depth of a successful branch. Without loss of generality,

925: assume the branch is of the form

926: 

927: $\quad$ $N_0:G_0\Rightarrow_{\theta_1,C_1}N_1:G_1\Rightarrow_{\theta_2,C_2} ...

928: \Rightarrow_{\theta_{d-1},C_{d-1}}N_{d-1}:G_{d-1}\Rightarrow_{\theta_d,C_d}\Box_t$

929: 

930: \noindent where $G_i=\leftarrow Q_i$ and $\theta=\theta_1...\theta_d$. 

931: We show, by induction on $0\leq k<d$, $WF(P) \models \forall 

932: (Q_k\theta_{k+1}...\theta_d)$.

933: 

934: Let $k=d-1$. Since $N_d$ is a success leaf, 

935: $G_{d-1}$ has only one literal, say $L$.

936: If $L$ is positive, $C_d$ must be a bodyless clause in $P$

937: such that $L\theta_d=C_d\theta_d$. In such a case, 

938: $WF(P) \models \forall (C_d)$, so that $WF(P) \models \forall (Q_k\theta_d)$.

939: Otherwise, $L=\neg A$ is a ground negative literal. By point 4 of Definition

940: \ref{slt-tree} $A\in TB_f$ and thus $WF(P) \models \neg A$. Therefore 

941: $WF(P) \models \forall (Q_k\theta_d)$ with $\theta_d=\emptyset$.

942: 

943: As induction hypothesis, assume that for $0<k<d$ $WF(P) \models \forall 

944: (Q_k\theta_{k+1}...\theta_d)$. We now prove $WF(P) \models \forall

945: (Q_{k-1}\theta_k\theta_{k+1}...\theta_d)$.

946: 

947: Let $G_{k-1}=\leftarrow L_1,...,L_n$

948: with $L_i$ being the selected literal. If $L_i=\neg A$ is negative,

949: $A$ must be ground and $A\in TB_f$ (otherwise either $N_{k-1}$ is a

950: flound leaf or a failure leaf, or $G_k$ contains a subgoal $u^*$

951: in which case $N_{k-1}$ will never lead to a success leaf). So

952: $WF(P) \models (L_i\theta_k)$ with $\theta_k=\emptyset$ and

953: $G_k=\leftarrow L_1,...,L_{i-1},L_{i+1},...,L_n$. 

954: By induction hypothesis we have

955: 

956: $\quad WF(P) \models \forall (Q_k

957: \theta_{k+1}...\theta_d) \Longrightarrow$\\

958: \indent $\quad WF(P) \models \forall ((L_1,...,L_{i-1},L_{i+1},...,L_n)

959: \theta_{k+1}...\theta_d) \Longrightarrow$\\

960: \indent $\quad WF(P) \models \forall ((L_1,...,L_{i-1},L_i,L_{i+1},...,L_n)

961: \theta_k\theta_{k+1}...\theta_d) \Longrightarrow$\\

962: \indent $\quad WF(P) \models \forall (Q_{k-1}\theta_k

963: \theta_{k+1}...\theta_d)$.

964: 

965: \noindent Otherwise, $L_i$ is positive. So there is a clause 

966: $L_i'\leftarrow B_1,...,B_m$ in $P$ with $L_i\theta_k=L_i'\theta_k$.

967: That is, $G_k=\leftarrow (L_1,...,L_{i-1},B_1,...,B_m,L_{i+1},...,L_n)\theta_k$.

968: Since $Q_k\theta_{k+1}...\theta_d$ is true in $WF(P)$, 

969: $(B_1,...,B_m)$ $\theta_k\theta_{k+1}...\theta_d$ is true in $WF(P)$.

970: So $L_i'\theta_k\theta_{k+1}...\theta_d$ is true in $WF(P)$. Therefore

971: 

972: $\quad WF(P) \models \forall (Q_k

973: \theta_{k+1}...\theta_d) \Longrightarrow$\\

974: \indent $\quad WF(P) \models \forall ((L_1,...,L_{i-1}, B_1,...,B_m, L_{i+1},...,L_n)\theta_k

975: \theta_{k+1}...\theta_d) \Longrightarrow$\\

976: \indent $\quad WF(P) \models \forall ((L_1,...,L_{i-1},L_i,L_{i+1},...,L_n)

977: \theta_k\theta_{k+1}...\theta_d) \Longrightarrow$\\

978: \indent $\quad WF(P) \models \forall (Q_{k-1}\theta_k

979: \theta_{k+1}...\theta_d)$. $\qquad\qquad\Box$

980: 

981: \vspace{4mm}

982: 

983: SLT-trees provide a basis for us to develop a sound 

984: and complete method for computing the well-founded semantics.

985: 

986: Observe that the concept of correct 

987: answer substitutions for a top goal $G_0$, defined in 

988: Definition \ref{branch}, can be extended to any goal 

989: $G_i$ at node $N_i$ in a generalized SLT-tree $GT_{G_0}$. 

990: This is done simply by adding a condition 

991: that the (sub-) branch starts at $N_i$. For instance, 

992: in Figure \ref{fig2} the branch that starts at $N_1$

993: and ends at $N_{15}$ yields a correct answer 

994: substitution $\theta_1\theta_2$ for the goal

995: $\leftarrow q(X)$ at $N_1$, where $\theta_1=\{X_1/X\}$ is the mgu of $q(X)$ unifying

996: with the head of $C_{q_3}$ and $\theta_2=\{X/a\}$ is the mgu of $p(X)$

997: at $N_5$ unifying with $C_{p_2}$. From the proof of Theorem \ref{ans-subs} 

998: it is easily seen that it

999: applies to correct answer substitutions for any goals in $GT_{G_0}$. 

1000: 

1001: Let $G_i$ be a goal in $GT_{G_0}$ and $L_j$ be the selected subgoal 

1002: in $G_i$. Assume that $L_j$ is positive. The partial branches of

1003: $GT_{G_0}$ that are used to prove $L_j$ constitute {\em sub-derivations}

1004: for $L_j$. By Theorem \ref{ans-subs}, for any correct answer substitution $\theta$ 

1005: built from a successful sub-derivation for $L_j$  

1006: $WF(P) \models \forall (L_j\theta)$. We refer to such intermediate results like

1007: $L_j\theta$ as {\em tabled positive answers}.

1008: 

1009: Let $TB_t^0$ consist of all tabled positive 

1010: answers in $GT_{G_0}$. Then $P$ is equivalent

1011: to $P^1=P\cup TB_t^0$ w.r.t. the well-founded 

1012: semantics. Due to the addition of

1013: tabled positive answers, a new generalized SLT-tree 

1014: $GT_{G_0}^1$ for $(P^1\cup \{G_0\},TB_f)$ can be built

1015: with possibly more tabled positive answers derived. 

1016: Let $TB_t^1$ consist of all tabled positive 

1017: answers in $GT_{G_0}^1$ but not in $TB_t^0$ 

1018: and $P^2=P^1\cup TB_t^1$. Clearly $P^2$ is equivalent

1019: to $P^1$ w.r.t. the well-founded semantics. 

1020: Repeating this process we will generate a sequence of equivalent programs

1021: 

1022: $\quad$ $P^1,P^2,...,P^i,...$

1023: 

1024: \noindent where $P^i=P^{i-1}\cup TB_t^{i-1}$ and 

1025: $TB_t^{i-1}$ consists of all tabled positive 

1026: answers in $GT_{G_0}^{i-1}$ for $(P^{i-1}\cup \{G_0\},TB_f)$ 

1027: but not in $\bigcup_{k=0}^{i-2} TB_t^k$, until we reach a fixpoint. 

1028: This leads to the following useful function.

1029: 

1030: \begin{definition}

1031: {\em

1032: Let $P$ be a program, $G_0$ a top goal and $R$ a computation rule. Define

1033: \begin{tabbing}

1034: {\bf function} $SLTP(P,G_0,R,TB_t,TB_f)$ {\bf return} 

1035: a generalized SLT-tree $GT_{G_0}$\\

1036: $\ $ \= {\bf begin} \\

1037: \> $\quad$ \= Build a generalized SLT-tree $GT_{G_0}$ 

1038: for $(P \cup \{G_0\},TB_f)$ via $R$;\\

1039: \>\> $NEW_t$ collects all tabled positive 

1040: answers in $GT_{G_0}$ but not in $TB_t$;\\

1041: \>\> {\bf if} \= $NEW_t = \emptyset$ {\bf then} return $GT_{G_0}$\\

1042: \>\> $\qquad$ {\bf else} return $SLTP(P\cup NEW_t,G_0,R,TB_t\cup NEW_t,TB_f)$\\ 

1043: \> {\bf end}

1044: \end{tabbing}

1045: }

1046: \end{definition}  

1047: 

1048: The following two theorems show that for 

1049: positive programs with the bounded-term-size property, 

1050: the function call $SLTP(P,G_0,R,\emptyset,\emptyset)$

1051: is terminating, and sound and complete w.r.t. the well-founded semantics.

1052: So we call it {\em SLTP-resolution} (i.e. SLT-resolution for 

1053: Positive programs).

1054: 

1055: \begin{theorem}

1056: \label{termin-positive}

1057: For positive programs with the bounded-term-size property 

1058: SLTP-resolution terminates in finite time.

1059: \end{theorem}

1060: 

1061: \noindent {\bf Proof:}

1062: The function call $SLTP(P,G_0,$ $R,\emptyset,\emptyset)$ will

1063: generate a sequence of generalized SLT-trees

1064: 

1065: $\quad$ $GT_{G_0}^0, GT_{G_0}^1,...,GT_{G_0}^i,...$

1066: 

1067: \noindent where $GT_{G_0}^0$ is the generalized 

1068: SLT-tree for $(P \cup \{G_0\},\emptyset)$ via $R$, 

1069: $GT_{G_0}^1$ is the generalized

1070: SLT-tree for $(P\cup NEW_t^0 \cup \{G_0\},\emptyset)$ via $R$ where

1071: $NEW_t^0$ consists of all tabled positive answers in $GT_{G_0}^0$, and

1072: $GT_{G_0}^i$ is the generalized SLT-tree for 

1073: $(P\cup NEW_t^0\cup NEW_t^1\cup ... \cup NEW_t^{i-1} 

1074: \cup \{G_0\},\emptyset)$ via $R$ where

1075: $NEW_t^{i-1}$ consists of all tabled positive answers in $GT_{G_0}^{i-1}$

1076: but not in $\bigcup_{k=0}^{i-2} NEW_t^k$.

1077: Since by Theorem \ref{tree-finite} the construction of each $GT_{G_0}^i$ is

1078: terminating, it suffices to prove that there exists an $i\geq 0$

1079: such that $NEW_t^i=\emptyset$.

1080: 

1081: Since $P$ has the bounded-term-size property and has only

1082: a finite number of clauses, we have only a finite number of 

1083: subgoals in all generalized SLT-trees $GT_{G_0}^i$s and

1084: any subgoal has only a finite number of positive answers (up to variable 

1085: renaming). Let $N$ be the number of all positive

1086: answers of all subgoals in all $GT_{G_0}^i$s.

1087: Since before the fixpoint is reached, from each $GT_{G_0}^i$ to $GT_{G_0}^{i+1}$

1088: at least one new tabled positive answer to some subgoal will be derived, 

1089: there must exist an $i\leq N+1$ such that $NEW_t^i=\emptyset$. $\Box$

1090: 

1091: \begin{theorem}

1092: \label{sound-comp-positive}

1093: Let $P$ be a positive program with the bounded-term-size property and 

1094: $G_0\leftarrow Q_0$ a top goal. Let $GT_{G_0}$

1095: be the generalized SLT-tree returned by

1096: $SLTP(P,G_0,$ $R,\emptyset,\emptyset)$. For any (Herbrand) ground instance 

1097: $Q_0\theta$ of $Q_0$ $WF(P)\models Q_0\theta$ 

1098: if and only if there is a correct answer substitution

1099: $\gamma$ for $G_0$ in $GT_{G_0}$ such that $\theta$ is an instance of 

1100: $\gamma$.

1101: \end{theorem}

1102: 

1103: The following lemma is required to prove this theorem.

1104: 

1105: \begin{lemma}

1106: \label{lemma1-positive}

1107: Let $GT_{G_0}^0,...,GT_{G_0}^i,...$ be 

1108: a sequence of generalized SLT-trees generated by 

1109: $SLTP($ $P,G_0,R,\emptyset,TB_f)$. For any $0\leq i <j$, if

1110: $\theta$ is a correct answer substitution for $G_0$ in $GT_{G_0}^i$,

1111: so is it in $GT_{G_0}^j$.

1112: \end{lemma}

1113: 

1114: \noindent {\bf Proof:}

1115: Assume that $GT_{G_0}^i$ and $GT_{G_0}^j$ are the 

1116: generalized SLT-trees for $(P\cup NEW_t \cup \{G_0\},TB_f)$ and

1117: $(P\cup NEW_t' \cup \{G_0\},TB_f)$, respectively. Then

1118: $NEW_t\subseteq NEW_t'$. Let 

1119: 

1120: $\quad$ $N_0:G_0\Rightarrow_{\theta_1,C_1}N_1:G_1\Rightarrow_{\theta_2,C_2} ...

1121: \Rightarrow_{\theta_{d-1},C_{d-1}}N_{d-1}:G_{d-1}\Rightarrow_{\theta_d,C_d}\Box_t$

1122: 

1123: \noindent be a successful branch in $GT_{G_0}^i$. At each derivation 

1124: step $N_{k-1}:G_{k-1}\Rightarrow_{\theta_k,C_k}N_k:G_k$, let $L$ be 

1125: the selected literal in $G_{k-1}$. If $L$ is a positive literal, $C_k$ 

1126: is either a clause in $P$ or a tabled positive answer in $NEW_t$; i.e. 

1127: $C_k\in P\cup NEW_t$ and thus $C_k\in P\cup NEW_t'$. So 

1128: $N_{k-1}:G_{k-1}\Rightarrow_{\theta_k,C_k}N_k:G_k$ must be in $GT_{G_0}^j$.

1129: Otherwise, $L=\neg A$ is a ground negative literal. In this case $A\in TB_f$ 

1130: (otherwise either $N_{k-1}$ is a failure leaf or $G_k$ contains a subgoal $u^*$

1131: in which case $N_{k-1}$ will never lead to a success leaf)

1132: and thus $N_{k-1}:G_{k-1}\Rightarrow_{\theta_k,

1133: C_k}N_k:G_k$ must be in $GT_{G_0}^j$ as well, where $\theta_k=\emptyset$

1134: and $C_k=\neg A$. Therefore, the above 

1135: successful branch will appear in $GT_{G_0}^j$. $\Box$

1136: 

1137: \vspace{4mm}

1138: 

1139: \noindent {\bf Proof of Theorem \ref{sound-comp-positive}:} 

1140: $(\Longleftarrow)$ 

1141: The function call $SLTP(P,G_0,$ $R,\emptyset,\emptyset)$ will

1142: generate a sequence of generalized SLT-trees

1143: 

1144: $\quad$ $GT_{G_0}^0, GT_{G_0}^1,...,GT_{G_0}^k=GT_{G_0}$

1145: 

1146: \noindent where $GT_{G_0}^0$ is the generalized 

1147: SLT-tree for $(P \cup \{G_0\},\emptyset)$, $GT_{G_0}^1$ is the generalized

1148: SLT-tree for $(P^1 \cup \{G_0\},\emptyset)$ with $P^1=P\cup NEW_t^0$, and

1149: $GT_{G_0}$ is the generalized SLT-tree for

1150: $(P^k\cup \{G_0\},\emptyset)$ with $P^k=P^{k-1}\cup NEW_t^{k-1}$ where 

1151: $NEW_t^{k-1}$ is all tabled positive answers in $GT_{G_0}^{k-1}$

1152: but not in $\bigcup_{i=0}^{k-2} NEW_t^i$. Since $NEW_t^i$s are

1153: sets of tabled positive answers, $P$ is equivalent to $P^1$ that

1154: is equivalent to $P^2$ that ... that is equivalent to $P^k$

1155: under the well-founded semantics. By Theorem \ref{ans-subs},

1156: for any correct answer substitution $\gamma$ for $G_0$ in $GT_{G_0}$

1157: $WF(P^k)\models \forall (Q_0\gamma)$ and thus

1158: $WF(P)\models \forall (Q_0\gamma)$.

1159: 

1160: $(\Longrightarrow)$ Assume $WF(P)\models Q_0\theta$.

1161: By the definition of the well-founded semantics, there

1162: must be a $\gamma$ more general than $\theta$ such that $Q_0\gamma$ 

1163: can be derived by iteratively applying some clauses in $P$. That is, 

1164: we have a backward chain of the form

1165: \begin{equation}

1166: \leftarrow Q_0\Rightarrow_{\theta_1,C_1}\leftarrow Q_1\Rightarrow_{\theta_2,C_2} ...

1167: \Rightarrow_{\theta_{d-1},C_{d-1}}\leftarrow Q_{d-1}\Rightarrow_{\theta_d,C_d}\Box

1168: \qquad\qquad\qquad \label{chain1}

1169: \end{equation}

1170: where $\gamma=\theta_1...\theta_d$ and the $C_i$s are in $P$. 

1171: We consider two cases.

1172: 

1173: Case 1: There is no loop or there are loops in (\ref{chain1})

1174: but no looping clauses are used. By Definition \ref{slt-tree}

1175: $GT_{G_0}^0$ must have a successful branch corresponding to (\ref{chain1}).

1176: By Lemma \ref{lemma1-positive} $GT_{G_0}$ contains such a branch, too.

1177: 

1178: Case 2: There are loops in (\ref{chain1}) with looping clauses applied.

1179: With no loss in generality, assume the backward chain (\ref{chain1}) corresponds to 

1180: the SLD-derivation shown in Figure \ref{fig-SC-positive}, where

1181: 

1182: \begin{enumerate}

1183: \item[(1)]

1184: The segments between $N_0$ and $N_{l_0}$ and between $N_{x_0}$ and $N_t$

1185: contain no loops. For any $0\leq i <m$ $p(\vec{X_i})$ is an ancestor variant 

1186: subgoal of $p(\vec{X}_{i+1})$. Obviously $C_{p_j}$ is a looping

1187: clause of $p(\vec{X}_{i+1})$ w.r.t. $p(\vec{X_i})$. 

1188: 

1189: \item[(2)]

1190: For $0\leq i <m$ from $N_{l_i}$ to $N_{l_{i+1}}$ 

1191: the proof of $p(\vec{X_i})$ reduces to 

1192: the proof of $(p(\vec{X}_{i+1}),B_{i+1})$ with

1193: a substitution $\theta_i$ for $p(\vec{X_i})$, where

1194: each $B_k$ $(0\leq k \leq m)$ is a set of subgoals. 

1195: 

1196: \item[(3)]

1197: The sub-derivation between $N_{l_m}$ and $N_{x_m}$ 

1198: contains no loops and yields an answer

1199: $p(\vec{X}_m)\gamma_m$ to $p(\vec{X}_m)$. The correct answer substitution

1200: $\gamma_m$ for $p(\vec{X}_m)$ is then applied to the remaining

1201: subgoals of $N_{l_m}$ (see node $N_{x_m}$), which leads to an answer

1202: $p(\vec{X}_{m-1})\gamma_m\gamma_{m-1}\theta_{m-1}$ to $p(\vec{X}_{m-1})$. 

1203: Such process continues recursively until an answer

1204: $p(\vec{X_0})\gamma_m...\gamma_0\theta_{m-1}...\theta_0$ to $p(\vec{X_0})$

1205: is produced at $N_{x_0}$.

1206: \end{enumerate} 

1207: 

1208: 

1209: \begin{figure}[htb]

1210: 

1211: \setlength{\unitlength}{3947sp}%

1212: %

1213: \begingroup\makeatletter\ifx\SetFigFont\undefined%

1214: \gdef\SetFigFont#1#2#3#4#5{%

1215:   \reset@font\fontsize{#1}{#2pt}%

1216:   \fontfamily{#3}\fontseries{#4}\fontshape{#5}%

1217:   \selectfont}%

1218: \fi\endgroup%

1219: \begin{picture}(3000,4095)(301,-4036)

1220: \thinlines

1221: \put(3226,-1186){\vector( 0,-1){225}}

1222: \put(3226,-586){\vector( 0,-1){225}}

1223: \put(3226,-1861){\vector( 0,-1){225}}

1224: \thicklines

1225: \multiput(3226,-166)(0.00000,-60.00000){3}{\makebox(6.6667,10.0000){\SetFigFont{10}{12}{\rmdefault}{\mddefault}{\updefault}.}}

1226: \multiput(3226,-1441)(0.00000,-60.00000){3}{\makebox(6.6667,10.0000){\SetFigFont{10}{12}{\rmdefault}{\mddefault}{\updefault}.}}

1227: \multiput(3226,-841)(0.00000,-60.00000){3}{\makebox(6.6667,10.0000){\SetFigFont{10}{12}{\rmdefault}{\mddefault}{\updefault}.}}

1228: \multiput(3226,-2116)(0.00000,-60.00000){3}{\makebox(6.6667,10.0000){\SetFigFont{10}{12}{\rmdefault}{\mddefault}{\updefault}.}}

1229: \multiput(3226,-2641)(0.00000,-60.00000){3}{\makebox(6.6667,10.0000){\SetFigFont{10}{12}{\rmdefault}{\mddefault}{\updefault}.}}

1230: \multiput(3226,-3166)(0.00000,-60.00000){3}{\makebox(6.6667,10.0000){\SetFigFont{10}{12}{\rmdefault}{\mddefault}{\updefault}.}}

1231: \multiput(3226,-3691)(0.00000,-60.00000){3}{\makebox(6.6667,10.0000){\SetFigFont{10}{12}{\rmdefault}{\mddefault}{\updefault}.}}

1232: \put(2926,-61){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_0:$ $\leftarrow Q_0$}}}

1233: \put(3301,-1336){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$C_{p_j}$}}}

1234: \put(1576,-511){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\qquad\qquad\qquad\quad$ $N_{l_0}:$ $\leftarrow p(\vec{X_0}),B_0$}}}

1235: \put(3301,-736){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$C_{p_j}$}}}

1236: \put(3301,-2011){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$C_{p_j}$}}}

1237: \put(301,-1786){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\qquad\qquad\qquad\quad$ $N_{l_m}:$ $\leftarrow p(\vec{X}_m),B_m,B_{m-1}\theta_{m-1},...,B_1\theta_{m-1}...\theta_1,B_0\theta_{m-1}...\theta_0$}}}

1238: \put(301,-2461){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\qquad\qquad\qquad\quad$ $N_{x_m}:$ $\leftarrow B_m\gamma_m,B_{m-1}\gamma_m\theta_{m-1},...,B_1\gamma_m\theta_{m-1}...\theta_1,B_0\gamma_m\theta_{m-1}...\theta_0$}}}

1239: \put(526,-2986){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\qquad\qquad\qquad\quad$ $N_{x_1}:$ $\leftarrow B_1\gamma_m...\gamma_1\theta_{m-1}...\theta_1,B_0\gamma_m...\gamma_1\theta_{m-1}...\theta_0$}}}

1240: \put(1351,-1111){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\qquad\qquad\qquad\quad$ $N_{l_1}:$ $\leftarrow p(\vec{X_1}),B_1,B_0\theta_0$}}}

1241: \put(1201,-3511){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\qquad\qquad\qquad\quad$ $N_{x_0}:$ $\leftarrow B_0\gamma_m...\gamma_0\theta_{m-1}...\theta_0$}}}

1242: \put(2851,-4036){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_t:$ $\Box$}}}

1243: \end{picture}

1244: 

1245: 

1246: \caption{An SLD-derivation with loops. $\qquad\qquad$}\label{fig-SC-positive}

1247: \end{figure} 

1248: 

1249: Since $C_{p_j}$ is a looping clause, the branch below $N_{l_1}$ via $C_{p_j}$

1250: will not occur in any SLT-trees. We first prove that a variant of the answer

1251: $p(\vec{X_0})\gamma_m...\gamma_0\theta_{m-1}...\theta_0$ 

1252: to $p(\vec{X_0})$ will be derived and used as a tabled positive

1253: answer by SLTP-resolution.

1254: 

1255: Since $p(\vec{X}_0)$ and $p(\vec{X}_m)$ are variants, the sub-derivation between

1256: $N_{l_m}$ and $N_{x_m}$ will appear directly below $N_{l_0}$

1257: via $C_{p_j}$ in $GT_{G_0}^0$, without going through $N_{l_1}$. 

1258: Thus a variant of the answer $p(\vec{X}_m)\gamma_m$ to $p(\vec{X}_m)$ 

1259: will be derived and added to $NEW_t^0$. 

1260: 

1261: Since $p(\vec{X}_0)$ and $p(\vec{X}_{m-1})$ are variants, 

1262: the sub-derivation between $N_{l_{m-1}}$ and $N_{x_{m-1}}$, where

1263: the sub-derivation between $N_{l_m}$ and $N_{x_m}$ is replaced by directly 

1264: using the tabled positive answer $p(\vec{X}_m)\gamma_m$ in $NEW_t^0$, 

1265: will appear directly below $N_{l_0}$

1266: via $C_{p_j}$ in $GT_{G_0}^1$, without going through $N_{l_1}$.

1267: Thus  a variant of the answer

1268: $p(\vec{X}_{m-1})\gamma_m\gamma_{m-1}\theta_{m-1}$ to $p(\vec{X}_{m-1})$

1269: will be derived and added to $NEW_t^1$.

1270: 

1271: Continue the above process iteratively. 

1272: After $n$ $(n\leq m)$ iterations, a variant of the answer

1273: $p(\vec{X_0})\gamma_m...\gamma_0\theta_{m-1}...\theta_0$ to $p(\vec{X_0})$

1274: will be derived in $GT_{G_0}^n$ and added to $NEW_t^n$.

1275: 

1276: Since by assumption there is no loop between $N_0$ 

1277: and $N_{l_0}$ and between $N_{x_0}$ and $N_t$, $GT_{G_0}^{n+1}$ must

1278: contain a successful branch corresponding to Figure \ref{fig-SC-positive}

1279: except that the sub-derivation between $N_{l_1}$ and $N_{x_0}$ is

1280: replaced by directly applying the tabled positive answer

1281: $p(\vec{X_0})\gamma_m...\gamma_0\theta_{m-1}...\theta_0$.

1282: This branch has the same correct answer substitution for $G_0$ as Figure

1283: \ref{fig-SC-positive} (up to variable renaming). By Lemma \ref{lemma1-positive} 

1284: $GT_{G_0}$ contains such a branch, too,

1285: so we conclude the proof. $\Box$

1286: 

1287: \vspace{4mm}

1288: 

1289: From the above proof it is easily seen that SLTP-resolution exhausts all tabled

1290: positive answers for all selected positive subgoals in $GT_{G_0}$. 

1291: The following result is immediate.

1292: 

1293: \begin{corollary}

1294: \label{corol1-positive}

1295: Let $P$ be a positive program with the bounded-term-size property,

1296: $G_0$ a top goal, and $GT_{G_0}$ the generalized SLT-tree 

1297: returned by $SLTP(P,G_0,R,\emptyset,\emptyset)$. Let $TB_t$ consist of

1298: all tabled positive answers in $GT_{G_0}$. Then

1299: \begin{enumerate}

1300: \item

1301: Let $A$ be a selected literal at some node in $GT_{G_0}$.

1302: For any (Herbrand) ground instance $A\theta$ of $A$

1303: $WF(P)\models A\theta$ if and only if there is a tabled answer $A'$ in $TB_t$

1304: such that $A\theta$ is an instance of $A'$.

1305: 

1306: \item

1307: Let $G_i=\leftarrow Q_i$ be a goal in $GT_{G_0}$. For any 

1308: (Herbrand) ground instance $Q_i\theta$ of $Q_i$

1309: $WF(P)\models Q_i\theta$ if and only if there is a correct answer substitution

1310: $\gamma$ for $G_i$ such that $\theta$ is an instance of $\gamma$.

1311: \end{enumerate}

1312: \end{corollary}

1313: 

1314: For a positive program, the well-founded semantics has a unique

1315: two-valued (minimal) model and the generalized SLT-tree $GT_{G_0}$ 

1316: returned by $SLTP(P,G_0,$ $R,\emptyset,\emptyset)$ contains only

1317: success and failure leaves. So the following result is immediate

1318: to Corollary \ref{corol1-positive}.

1319: 

1320: \begin{corollary}

1321: \label{corol2-positive}

1322: Let $P$ be a positive program with the bounded-term-size property,

1323: $G_0$ a top goal, and 

1324: $GT_{G_0}$ the generalized SLT-tree

1325: returned by $SLTP(P,G_0,R,\emptyset,\emptyset)$.

1326: For any goal $G_i=\leftarrow Q_i$ at some node $N_i$ in $GT_{G_0}$, if

1327: all branches starting at $N_i$ end with a failure leaf

1328: then $WF(P) \models \neg\exists (Q_i)$.

1329: \end{corollary}

1330:  

1331: Apparently Corollary \ref{corol2-positive} 

1332: does not hold with general logic programs because

1333: their generalized SLT-trees may contain temporarily undefined leaves.

1334: For instance, although $N_{10}$ labeled by $\leftarrow r$ in Figure \ref{fig2}

1335: ends only with a failure leaf, $r$ is not false in $WF(P_1)$ 

1336: because it has another sub-derivation in $GT_{\leftarrow p(X)}$,

1337: $N_6\rightarrow N_7\rightarrow N_{12}$, that ends with a

1338: temporarily undefined leaf. However, it turns out that the ground atom $w$ in

1339: Figure \ref{fig2} is false in $WF(P_1)$ because all its sub-derivations

1340: (i.e., $N_{16}$ and $N_4\rightarrow N_{14}\rightarrow N_{17}$)

1341: end with a failure leaf. This observation is supported by 

1342: the following theorem.

1343: 

1344: \begin{theorem}

1345: \label{main-th1}

1346: Let $P$ be a program with the bounded-term-size property and 

1347: $GT_{G_0}$ the generalized SLT-tree returned by 

1348: $SLTP(P,G_0,R,\emptyset,\emptyset)$. Let $TB_t$ consist of all 

1349: tabled positive answers in $GT_{G_0}$

1350: 

1351: \begin{enumerate}

1352: 

1353: \item

1354: For any selected positive literal $A$ in $GT_{G_0}$, 

1355: $A\theta\in M_P(\emptyset)$ if and only if there 

1356: is a correct answer substitution for

1357: $A$ in $GT_{G_0}$ that is more general than $\theta$

1358: if and only if there is an $A'\in TB_t$

1359: with $A\theta$ as an instance. In particular, when $A$ is ground,

1360: $A\in M_P(\emptyset)$ if and only if $A\in TB_t$.

1361: 

1362: \item

1363: Let $A$ be a selected ground positive 

1364: literal in $GT_{G_0}$. Let $S$ be the set of

1365: selected subgoals at the leaf nodes of all

1366: sub-derivations for $A$. $A\in N_P(\emptyset)$

1367: if and only if all sub-derivations for $A$ and $S$ 

1368: end with a failure leaf. 

1369: \end{enumerate}

1370: \end{theorem}

1371: 

1372: \noindent {\bf Proof:} 1. Note that clauses with negative literals in

1373: their bodies do not contribute to deriving positive answers in $M_P(\emptyset)$

1374: (see Definition \ref{trans-ops1}). This is true in

1375: $SLTP(P,G_0,R,\emptyset,\emptyset)$ as well because a selected  

1376: subgoal $\neg B$ either fails (when $B$ succeeds) or  

1377: is temporarily undefined (otherwise). Let $P^+$ be a positive program

1378: obtained from $P$ by removing all clauses with negative literals in their bodies.

1379: Then $M_P(\emptyset)=M_{P^+}(\emptyset)$ and all tabled positive

1380: answers in $GT_{G_0}$ are derived from $P^+\cup \{G_0\}$. Since

1381: $M_{P^+}(\emptyset)$ is the positive part of $WF(P^+)$, we have

1382: \begin{tabbing}

1383: $\qquad A\theta\in M_P(\emptyset)$\= $\Longleftrightarrow 

1384: A\theta\in M_{P^+}(\emptyset)$ \\

1385: \> $\Longleftrightarrow WF(P^+)\models A\theta$ \\

1386: \> $\Longleftrightarrow$ \= (By Corollary \ref{corol1-positive})

1387: there is an answer substitution for $A$ in $GT_{G_0}$ \\

1388: \>\> that is more general than $\theta$\\

1389: \>  $\Longleftrightarrow$ there is an $A'\in TB_t$

1390: with $A\theta$ as an instance.

1391: \end{tabbing}

1392: When $A$ is ground,

1393: \begin{tabbing}

1394: $\qquad A\in M_P(\emptyset)$\= $\Longleftrightarrow$ 

1395: there is an answer substitution for $A$ in $GT_{G_0}$ \\

1396: \> $\Longleftrightarrow$ (By Definition \ref{branch}) 

1397: there is a successful sub-derivation for $A$ in $GT_{G_0}$ \\

1398: \> $\Longleftrightarrow$ $A\in TB_t$.

1399: \end{tabbing}

1400: 

1401: 2. $(\Longleftarrow)$ By point 1 above $A\not\in M_P(\emptyset)$.

1402: Suppose, on the contrary, that $A\in O_P(\emptyset)$.

1403: Then by Definition \ref{vp} there exists a clause $C$ in $P$ of the form

1404: 

1405: $\qquad A'\leftarrow B_1,...,B_m, \neg D_1,...,\neg D_n$

1406: 

1407: \noindent such that one of its Herbrand instantiated clauses is of the form

1408: 

1409: $\qquad A\leftarrow (B_1,...,B_m, \neg D_1,...,\neg D_n)\theta$

1410: 

1411: \noindent where no $D_i\theta$ is in $M_P(\emptyset)$ and each $B_i\theta$ is

1412: either in $M_P(\emptyset)$ or in $O_P(\emptyset)$. That is, $A$ can be derived

1413: through a backward chain of the form

1414: 

1415: $\qquad A\Rightarrow_{S_1} B_1\theta,...,B_m\theta,\neg D_1\theta,

1416: ...,\neg D_n\theta\Rightarrow_{S_2}

1417: E_1,...,\neg F_k\Rightarrow_{S_3}...\Rightarrow_{S_t}\Box$

1418: 

1419: \noindent where each step is performed by either 

1420: resolving a ground positive literal

1421: like $B_i\theta$ with an answer in $M_P(\emptyset)$ (if $B_i\theta

1422: \in M_P(\emptyset)$) or

1423: with a Herbrand instantiated clause of $P$ (otherwise),

1424: or removing a negative literal like

1425: $\neg D_i\theta$ where $D_i\theta\not\in M_P(\emptyset)$.

1426: 

1427: Based on point 1 above, it is easy to construct a sub-derivation for $A$,

1428: using clauses in $P$ and tabled answers in $TB_t$,

1429: that corresponds to the above backward chain. First we have

1430: 

1431: $\qquad\leftarrow A\Rightarrow_{C,\theta_0}

1432: \leftarrow B_1\theta_0,...,B_m\theta_0,\neg D_1\theta_0,

1433: ...,\neg D_n\theta_0$

1434: 

1435: \noindent where $\theta_0$ is the most general unifier of $A$ and $A'$.

1436: For each $B_i\theta_0$, if

1437: $B_i\theta$ is resolved with a Herbrand instantiated clause of $P$

1438: (resp. with an answer in $M_P(\emptyset)$) then there is a clause in $P$

1439: (resp. a tabled positive answer in $TB_t$) to resolve with 

1440: $B_i\theta_0$. For each $\neg D_i\theta_0$, if $\theta_0=\theta$

1441: then $\neg D_i\theta_0$ is treated as $u^*$. 

1442: As a result, we will generate a sub-derivation for $A$

1443: of the form

1444: 

1445: $\qquad \leftarrow A\Rightarrow_{C,\theta_0}...\Rightarrow_{C_{i-1},

1446: \theta_{i-1}}\leftarrow L_1,L_2,...,L_k \Rightarrow_{C_i,\theta_i}...

1447: \Rightarrow_{C_l,\theta_l} \Box_{u^*}$

1448: 

1449: If no looping clause is used along the above sub-derivation for $A$,

1450: this sub-derivation must be in $GT_{G_0}$. Otherwise, without 

1451: loss of generality assume the above sub-derivation is of the form

1452: 

1453: \noindent $\quad \leftarrow A\Rightarrow_{C,\theta_0}...

1454: \leftarrow L_1,L_2,...,L_k \Rightarrow_{C_i,\theta_i}...

1455: \leftarrow L_1',F_1,...,F_j,(L_2,...,L_k)\gamma\Rightarrow_{C_i,\theta_i'}

1456: ...\Rightarrow_{C_l,\theta_l} \Box_{u^*}$ 

1457: 

1458: \noindent where $L_1$ is an ancestor variant subgoal of $L_1'$

1459: and $L_1'$ is selected to resolve with the looping clause $C_i$.

1460: It is easily seen that this sub-derivation can be shortened by removing

1461: the sub-derivation between $L_1$ and $L_1'$ because if 

1462: $L_1',F_1,...,F_j,(L_2,...,L_k)\gamma$ can be reduced to $\Box_{u^*}$,

1463: so can $L_1,L_2,...,L_k$. Obviously, the shortened sub-derivation

1464: (or its variant form) will appear in $GT_{G_0}$. 

1465: This contradicts that all sub-derivations of $A$ and $S$ in 

1466: $GT_{G_0}$ end with a failure leaf.  

1467: 

1468: $(\Longrightarrow)$ Assume $A\in N_P(\emptyset)$ but, on the contrary, that

1469: there is a sub-derivation for $A$ in $GT_{G_0}$ that ends with

1470: a temporarily undefined leaf. Let the sub-derivation be of the form

1471: 

1472: $\qquad \leftarrow A\Rightarrow_{C,\theta_0}...\Rightarrow_{C_{i-1},

1473: \theta_{i-1}}\leftarrow L_1,L_2,...,L_k \Rightarrow_{C_i,\theta_i}...

1474: \Rightarrow_{C_l,\theta_l} \Box_{u^*}$

1475: 

1476: \noindent where each derivation step is done by either resolving 

1477: a selected positive literal with a clause in $P$ or with a tabled positive 

1478: answer in $TB_t$, or treating a selected negative ground literal 

1479: $\neg F$ as $u^*$ where $F\not\in TB_t$. Since by point 1 of this theorem

1480: $M_P(\emptyset)$ consists of all (Herbrand) ground instances of 

1481: tabled positive answer in $TB_t$, the above

1482: sub-derivation must have a Herbrand instantiated ground instance of the form

1483: 

1484: $\qquad A\Rightarrow_{S_1} ...\Rightarrow_{S_j} E_1,...,E_m, 

1485: \neg F_1,...,\neg F_n\Rightarrow_{S_{j+1}}...\Rightarrow_{S_t}\Box$

1486: 

1487: \noindent where each step is performed by either resolving a positive ground

1488: literal with a Herbrand instantiated clause of $P$ or with

1489: an answer in $M_P(\emptyset)$, or removing a negative ground literal 

1490: $\neg F$ where $F\not\in M_P(\emptyset)$. However, by Definition \ref{vp}

1491: the above backward chain implies that $A$ is in $O_P(\emptyset)$, 

1492: contradicting $A\in N_P(\emptyset)$. 

1493: 

1494: Now assume that $A\in N_P(\emptyset)$ and 

1495: all sub-derivations for $A$ end with a failure leaf,

1496: but, on the contrary, that there is a sub-derivation 

1497: for $B\in S$ in $GT_{G_0}$ that ends with a temporarily 

1498: undefined leaf. Then $B$ must be an ancestor subgoal

1499: of $B$. That is, there must be two sub-derivations

1500: for $B$ in $GT_{G_0}$ of the form

1501: 

1502: $\qquad \leftarrow B\Rightarrow ...

1503: \leftarrow A, ... \Rightarrow...

1504: \Rightarrow \Box_f \leftarrow B, ...$

1505: 

1506: $\qquad \leftarrow B\Rightarrow ... 

1507: \Rightarrow \Box_{u^*}$

1508: 

1509: \noindent The first sub-derivation suggests that

1510: the answers of $A$ depend on $B$. By the first part of

1511: the argument for $(\Longrightarrow)$, the second 

1512: sub-derivation implies $B \not\in N_P(\emptyset)$.

1513: Combining the two leads to $A \not\in N_P(\emptyset)$, 

1514: which contradicts the assumption $A \in N_P(\emptyset)$.

1515: $\Box$

1516: 

1517: \vspace{4mm}

1518: 

1519: Theorem \ref{main-th1} is useful, by which the truth value of all 

1520: selected ground negative literals can be determined in an iterative way.

1521: For any selected ground negative literal $\neg A$, if 

1522: all sub-derivations of $A$  and $S$ (defined in Theorem \ref{main-th1})

1523: in $GT_{G_0}$ end with a failure leaf, 

1524: $A$ is called a {\em tabled negative answer}. All tabled negative

1525: answers will be collected in $TB_f$. 

1526: 

1527: We are now in a position to define SLT-resolution for general 

1528: logic programs.

1529: 

1530: \begin{definition}[SLT-resolution]

1531: \label{slt}

1532: {\em

1533: Let $P$ be a program, $G_0$ a top goal and $R$ a computation rule. 

1534: {\em SLT-resolution} proves $G_0$ by calling the function 

1535: $SLT(P,G_0,R,\emptyset,\emptyset)$, which is defined as follows:

1536: \begin{tabbing}

1537: {\bf function} $SLT(P,G_0,R,TB_t, TB_f)$ {\bf return} a 

1538: generalized SLT-tree $GT_{G_0}$\\

1539: $\ $ \= {\bf begin} \\

1540: \> $\quad$ \= $GT_{G_0}=SLTP(P,G_0,R,TB_t,TB_f)$; \\

1541: \>\>  $NEW_t$ collects all tabled positive answers in $GT_{G_0}$ 

1542: but not in $TB_t$;\\

1543: \>\>  $NEW_f$ collects all tabled negative answers in $GT_{G_0}$ 

1544: but not in $TB_f$;\\

1545: \>\> {\bf if} \= $NEW_f = \emptyset$ {\bf then} return $GT_{G_0}$\\

1546: \>\> $\qquad$ {\bf else} return $SLT(P\cup NEW_t,G_0,R,TB_t\cup 

1547: NEW_t,TB_f\cup NEW_f)$ \\

1548: \> {\bf end} 

1549: \end{tabbing}

1550: }

1551: \end{definition} 

1552: 

1553: \begin{definition}

1554: \label{true-false}

1555: {\em

1556: Let $G_0=\leftarrow Q_0$ be a top goal and

1557: $T_{G_0}$ be the top SLT-tree in $GT_{G_0}$ which is returned by 

1558: $SLT(P,G_0,R,\emptyset,\emptyset)$. $G_0$ is {\em true} in $P$ with an

1559: answer $Q_0\theta$ if there is a correct answer substitution for

1560: $G_0$ in $T_{G_0}$ that is more general than $\theta$;

1561: {\em false} in $P$ if all branches of $T_{G_0}$ end with a failure

1562: leaf; {\em undefined} in $P$ if neither $G_0$ is false nor $T_{G_0}$

1563: has successful branches.

1564: }

1565: \end{definition} 

1566: 

1567: \begin{example}

1568: \label{eg3-3}

1569: {\em

1570: (Cont. of Example \ref{eg3-2}) To evaluate $G_0=\leftarrow p(X)$,

1571: we call $SLT(P_1,G_0,R,\emptyset,\emptyset)$. This

1572: immediately invokes $SLTP(P_1,G_0,R,\emptyset,\emptyset)$, which generates

1573: the generalized SLT-tree $GT_{\leftarrow p(X)}$ for 

1574: $(P_1\cup \{\leftarrow p(X)\},\emptyset)$

1575: as shown in Figure \ref{fig2}. The tabled positive answers in

1576: $GT_{\leftarrow p(X)}$ are then  collected in $NEW_t^0$,

1577: i.e. $NEW_t^0=\{p(a),q(a)\}$. So $P_1^1=P_1\cup NEW_t^0$. (Note that 

1578: the bodyless program clause $C_{p_2}$ can be ignored in $P_1^1$ since it has

1579: become a tabled answer. See Section \ref{sec-dup} for such kind of optimizations). 

1580: The generalized SLT-tree $GT_{\leftarrow p(X)}^1$ for 

1581: $(P_1^1\cup \{\leftarrow p(X)\},\emptyset)$ is then generated, which is like

1582: $GT_{\leftarrow p(X)}$ except that $N_2$ gets a new child node $N_{2'}$ $-$ a

1583: success leaf, by unifying $q(X)$ with the tabled positive answer $q(a)$ 

1584: in $P_1^1$ (see Figure \ref{fig3}).

1585: Clearly, the addition of this success leaf does not yield any new 

1586: tabled positive answers, i.e. $NEW_t^1=\emptyset$. Therefore 

1587: $SLTP(P_1,G_0,R,\emptyset,\emptyset)$ returns $GT_{\leftarrow p(X)}^1$.

1588: 

1589: \begin{figure}[htb]

1590: \centering

1591: 

1592: \setlength{\unitlength}{3947sp}%

1593: %

1594: \begingroup\makeatletter\ifx\SetFigFont\undefined%

1595: \gdef\SetFigFont#1#2#3#4#5{%

1596:   \reset@font\fontsize{#1}{#2pt}%

1597:   \fontfamily{#3}\fontseries{#4}\fontshape{#5}%

1598:   \selectfont}%

1599: \fi\endgroup%

1600: \begin{picture}(4062,3321)(1051,-3286)

1601: \thinlines

1602: \put(3315,-560){\vector(-4,-1){529.412}}

1603: \put(4951,-1111){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$p(a)$}}}

1604: \put(2701,-586){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$q(a)$}}}

1605: \put(2251,-211){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$p(a)$}}}

1606: \put(3601,-561){\vector(-2,-1){380}}

1607: \put(3901,-561){\vector( 2,-1){380}}

1608: \put(3751,-561){\vector( 0,-1){200}}

1609: \put(2621,-1226){\vector(-2,-1){0}}

1610: \multiput(3001,-1036)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

1611: \put(3751,-1036){\vector( 0,-1){200}}

1612: \put(2476,-1486){\vector( 0,-1){200}}

1613: \put(1946,-2126){\vector(-2,-1){0}}

1614: \multiput(2326,-1936)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

1615: \put(1876,-2386){\vector( 0,-1){200}}

1616: \put(2026,-2836){\vector( 2,-1){380}}

1617: \put(4726,-1036){\vector( 2,-1){380}}

1618: \put(4051,-1486){\vector( 2,-1){380}}

1619: \put(2551,-1936){\vector( 2,-1){380}}

1620: \put(3151,-1036){\vector( 0,-1){200}}

1621: \put(3371,-1676){\vector(-2,-1){0}}

1622: \multiput(3751,-1486)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

1623: \put(1421,-3026){\vector(-2,-1){0}}

1624: \multiput(1801,-2836)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

1625: \put(3301,-136){\vector( 2,-1){380}}

1626: \put(2776,-136){\vector(-2,-1){380}}

1627: \put(3451,-961){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_4:$ $w$ }}}

1628: \put(4051,-961){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_5:$ $p(X)$ }}}

1629: \put(2251,-1411){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_6:$ $ r$ }}}

1630: \put(3826,-1186){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{w_1}$}}}

1631: \put(3451,-1411){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{14}:$ $\neg w,v$ }}}

1632: \put(2551,-1636){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{r_1}$}}}

1633: \put(2101,-1861){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_7:$ $\neg s$ }}}

1634: \put(1651,-2311){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_8:$ $s$ }}}

1635: \put(1951,-2536){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{s_1}$}}}

1636: \put(1501,-2761){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_9:$ $\neg r$ }}}

1637: \put(3226,-1786){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

1638: \put(3001,-1936){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{16}:$ $w$ }}}

1639: \put(4051,-1936){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{17}:$ $v, u^*$ }}}

1640: \put(1051,-3286){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{10}:$ $r$ }}}

1641: \put(5026,-1486){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{15}:$}}}

1642: \put(5101,-1336){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_t$}}}

1643: \put(4426,-1786){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

1644: \put(2926,-2236){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_{u^*}$ }}}

1645: \put(2851,-2386){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{12}:$ $u^*$ }}}

1646: \put(1276,-3136){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

1647: \put(2401,-3136){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_{u^*}$ }}}

1648: \put(2326,-3286){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{11}:$ $u^*$ }}}

1649: \put(2851,-1561){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{13}:$ $u^*$ }}}

1650: \put(3076,-1411){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_{u^*}$ }}}

1651: \put(3301,-511){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_2:$  $q(X)$}}}

1652: \put(2776,-961){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_3:$ $\neg r$ }}}

1653: \put(2551,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_t$}}}

1654: \put(2326,-961){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{2'}:$}}}

1655: \put(2701,-61){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_0:$ $p(X)$ }}}

1656: \put(3526,-211){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{p_1}$}}}

1657: \put(2251,-436){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_t$}}}

1658: \put(2026,-586){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_1:$}}}

1659: \put(3451,-736){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$C_{q_2}$}}}

1660: \put(3001,-736){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$C_{q_1}$}}}

1661: \put(4201,-661){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{q_3}$}}}

1662: \end{picture}

1663: 

1664: \caption{The generalized SLT-tree $GT_{\leftarrow p(X)}^1$ for 

1665: $(P_1^1\cup \{\leftarrow p(X)\},\emptyset)$. $\qquad\qquad$}\label{fig3}

1666: \end{figure} 

1667: 

1668: It is easily seen that $GT_{\leftarrow p(X)}^1$ contains one new

1669: tabled negative answer $w$; i.e. $NEW_f^1=\{w\}$ (note 

1670: that $\neg w$ is a selected literal at $N_{14}$ and all sub-derivations 

1671: for $w$ in $GT_{\leftarrow p(X)}^1$ end with a failure leaf).

1672: Let $TB_t^1=NEW_t^0\cup NEW_t^1$ and $TB_f^1=NEW_f^1$.

1673: Since $NEW_f^1\neq\emptyset$, $SLT(P_1\cup TB_t^1,G_0,R, 

1674: TB_t^1,TB_f^1)$ is recursively called, which invokes 

1675: $SLTP(P_1\cup TB_t^1,G_0,R,$ $TB_t^1,TB_f^1)$. This builds

1676: a generalized SLT-tree $GT_{\leftarrow p(X)}^2$ for 

1677: $(P_1^2\cup \{\leftarrow p(X)\},TB_f^1)$

1678: where $P_1^2=P_1\cup TB_t^1$ (see Figure \ref{fig4}). 

1679: Obviously, $GT_{\leftarrow p(X)}^2$ contains neither new tabled

1680: positive answers nor new tabled negative answers. Therefore,

1681: SLT-resolution stops with $GT_{\leftarrow p(X)}^2$ returned.

1682: By Definition \ref{true-false}, $G_0$ is true with an

1683: answer $p(a)$.

1684: }

1685: \end{example}

1686: 

1687: \begin{figure}[htb]

1688: \centering

1689: 

1690: \setlength{\unitlength}{3947sp}%

1691: %

1692: \begingroup\makeatletter\ifx\SetFigFont\undefined%

1693: \gdef\SetFigFont#1#2#3#4#5{%

1694:   \reset@font\fontsize{#1}{#2pt}%

1695:   \fontfamily{#3}\fontseries{#4}\fontshape{#5}%

1696:   \selectfont}%

1697: \fi\endgroup%

1698: \begin{picture}(4062,3321)(1051,-3286)

1699: \thinlines

1700: \put(3315,-560){\vector(-4,-1){529.412}}

1701: \put(4951,-1111){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$p(a)$}}}

1702: \put(2701,-586){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$q(a)$}}}

1703: \put(2251,-211){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$p(a)$}}}

1704: \put(4351,-1636){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\neg w$}}}

1705: \put(3601,-561){\vector(-2,-1){380}}

1706: \put(3901,-561){\vector( 2,-1){380}}

1707: \put(3751,-561){\vector( 0,-1){200}}

1708: \put(2621,-1226){\vector(-2,-1){0}}

1709: \multiput(3001,-1036)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

1710: \put(3751,-1036){\vector( 0,-1){200}}

1711: \put(2476,-1486){\vector( 0,-1){200}}

1712: \put(1946,-2126){\vector(-2,-1){0}}

1713: \multiput(2326,-1936)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

1714: \put(1876,-2386){\vector( 0,-1){200}}

1715: \put(2026,-2836){\vector( 2,-1){380}}

1716: \put(4726,-1036){\vector( 2,-1){380}}

1717: \put(4051,-1486){\vector( 2,-1){380}}

1718: \put(2551,-1936){\vector( 2,-1){380}}

1719: \put(3151,-1036){\vector( 0,-1){200}}

1720: \put(1421,-3026){\vector(-2,-1){0}}

1721: \multiput(1801,-2836)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

1722: \put(3301,-136){\vector( 2,-1){380}}

1723: \put(2776,-136){\vector(-2,-1){380}}

1724: \put(3451,-961){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_4:$ $w$ }}}

1725: \put(4051,-961){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_5:$ $p(X)$ }}}

1726: \put(2251,-1411){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_6:$ $ r$ }}}

1727: \put(3826,-1186){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{w_1}$}}}

1728: \put(3451,-1411){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{14}:$ $\neg w,v$ }}}

1729: \put(2551,-1636){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{r_1}$}}}

1730: \put(2101,-1861){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_7:$ $\neg s$ }}}

1731: \put(1651,-2311){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_8:$ $s$ }}}

1732: \put(1951,-2536){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{s_1}$}}}

1733: \put(1501,-2761){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_9:$ $\neg r$ }}}

1734: \put(4051,-1936){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{17}:$ $v, u^*$ }}}

1735: \put(1051,-3286){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{10}:$ $r$ }}}

1736: \put(5026,-1486){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{15}:$}}}

1737: \put(5101,-1336){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_t$}}}

1738: \put(4426,-1786){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

1739: \put(2926,-2236){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_{u^*}$ }}}

1740: \put(2851,-2386){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{12}:$ $u^*$ }}}

1741: \put(1276,-3136){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

1742: \put(2401,-3136){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_{u^*}$ }}}

1743: \put(2326,-3286){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{11}:$ $u^*$ }}}

1744: \put(2851,-1561){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{13}:$ $u^*$ }}}

1745: \put(3076,-1411){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_{u^*}$ }}}

1746: \put(3301,-511){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_2:$  $q(X)$}}}

1747: \put(2776,-961){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_3:$ $\neg r$ }}}

1748: \put(2551,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_t$}}}

1749: \put(2326,-961){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{2'}:$}}}

1750: \put(2701,-61){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_0:$ $p(X)$ }}}

1751: \put(3526,-211){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{p_1}$}}}

1752: \put(2251,-436){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_t$}}}

1753: \put(2026,-586){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_1:$}}}

1754: \put(3451,-736){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$C_{q_2}$}}}

1755: \put(3001,-736){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$C_{q_1}$}}}

1756: \put(4201,-661){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{q_3}$}}}

1757: \end{picture}

1758: 

1759: 

1760: \caption{The generalized SLT-tree $GT_{\leftarrow p(X)}^2$ for 

1761: $(P_1^2\cup \{\leftarrow p(X)\},TB_f^1)$. $\qquad\qquad$}\label{fig4}

1762: \end{figure} 

1763: 

1764: \section{Soundness and Completeness of SLT-resolution}

1765: In this section we establish the termination, 

1766: soundness and completeness of SLT-resolution.

1767: 

1768: \begin{theorem}

1769: \label{termin-normal}

1770: For programs with the bounded-term-size property

1771: SLT-resolution terminates in finite time.

1772: \end{theorem}

1773: 

1774: \noindent {\bf Proof:}

1775: Let $P$ be a program with the bounded-term-size property. Since $P$ 

1776: has only a finite number of clauses, we have only a finite number,

1777: say $N$, of ground subgoals in all generalized SLT-trees $GT_{G_0}^i$s. 

1778: Before SLT-resolution stops, in each new recursion via $SLT()$

1779: at least one new tabled negative answer will be derived.

1780: Therefore, there are at most $N$ recursions in SLT-resolution.

1781: By Theorem \ref{termin-positive}, each recursion (i.e. the execution

1782: of $SLTP()$) will terminate in finite time, so we conclude the proof. $\Box$

1783: 

1784: \vspace{4mm}

1785: 

1786: By Theorem \ref{termin-normal},

1787: for programs with the bounded-term-size property, by calling

1788: $SLT(P,$ $G_0,R,\emptyset,\emptyset)$ SLT-resolution

1789: generates a finite sequence of generalized SLT-trees:

1790: \begin{eqnarray}

1791: GT_{G_0}^1 & = & SLTP(P,G_0,R,\emptyset,\emptyset), \nonumber\\

1792: GT_{G_0}^2 & = & SLTP(P^1,G_0,R,TB_t^1,TB_f^1), \qquad\qquad\qquad\nonumber \\

1793:            & \vdots \label{seq} & \label{sequence}\\

1794: GT_{G_0}^{k+1} & = & SLTP(P^k,G_0,R,TB_t^k,TB_f^k) \nonumber, 

1795: \end{eqnarray}

1796: where for each $1\leq i\leq k$, 

1797: $P^i=P\cup TB_t^i$, and $TB_t^i$ and $TB_f^i$ respectively consist of 

1798: all tabled positive and negative answers 

1799: in all $GT_{G_0}^j$s $(j\leq i)$. $GT_{G_0}^{k+1}$

1800: will be returned since it contains no new tabled answers

1801: (see Definition \ref{slt}).

1802: 

1803: To simplify our presentation, in the following lemmas/corollaries/theorems, 

1804: we assume that $P$ is a program with the bounded-term-size property, $G_0$

1805: is a top goal, $GT_{G_0}=GT_{G_0}^{k+1}$ is as defined in (\ref{sequence}), 

1806: and $T_{G_0}$ is the top SLT-tree in $GT_{G_0}$.

1807: 

1808: \begin{lemma}

1809: \label{sc-lem}

1810: Let $GT_{G_0}^i$ $(i\geq 1)$ be as defined in (\ref{sequence}).

1811: For any selected ground subgoal $A$ in $GT_{G_0}^{i+1}$,

1812: if $A$ is in $TB_f^i$ then all sub-derivations for $A$ in 

1813: $GT_{G_0}^{i+1}$ will end with a failure leaf.

1814: \end{lemma}

1815: 

1816: \noindent {\bf Proof:} $A\in TB_f^i$ indicates that if $A$ is 

1817: a selected ground subgoal in $GT_{G_0}^i$, all its sub-derivations

1818: end with a failure leaf. This implies that the truth value of $A$ 

1819: does not depend on any selected negative subgoals whose truth values are

1820: temporarily undefined in $GT_{G_0}^i$. Since $GT_{G_0}^{i+1}$ is derived

1821: from $GT_{G_0}^i$ simply by treating some selected negative subgoals $\neg B$

1822: whose truth values are temporarily undefined in $GT_{G_0}^i$ as true by

1823: assuming $B$ is false, such process obviously will not affect the truth value

1824: of $A$. Therefore, all sub-derivations for $A$ in $GT_{G_0}^{i+1}$ will

1825: end with a failure leaf. $\Box$

1826: 

1827: \begin{lemma}

1828: \label{sc-lem1}

1829: $\qquad$

1830: \begin{enumerate}

1831: \item

1832: For any selected positive literal $A$ in $GT_{G_0}$,

1833: there is a correct answer substitution $\gamma$ for $A$ in $GT_{G_0}$

1834: if and only if $A\gamma\in TB_t^k$ (up to variable renaming).

1835: \item

1836: For any selected positive literal $A$ at any node $N_i$ in $T_{G_0}$,

1837: there is a correct answer substitution $\gamma$ for $A$ in $GT_{G_0}$

1838: if and only if there is a correct answer substitution $\gamma$ for $A$ 

1839: at node $N_i$ in $T_{G_0}$ (up to variable renaming).

1840: \end{enumerate}

1841: \end{lemma}

1842: 

1843: \noindent {\bf Proof:}

1844: Point 1 is straightforward by the fact that

1845: $GT_{G_0}$ contains no new tabled positive answers. By point 1,

1846: all correct answer substitutions for $A$ in $GT_{G_0}$ are in $TB_t^k$. 

1847: Hence point 2 follows immediately from the fact that the selected literal 

1848: $A$ at node $N_i$ in $T_{G_0}$ will

1849: use all tabled answers in $TB_t^k$ that unify with $A$. $\Box$

1850: 

1851: \begin{lemma}

1852: \label{sc-lem2}

1853: For any selected positive literal $A$ in $GT_{G_0}$, 

1854: $A\theta\in M_{P^k}(\neg .TB_f^k)$ if and only if there 

1855: is a correct answer substitution for

1856: $A$ in $GT_{G_0}$ that is more general than $\theta$, and 

1857: for any selected ground positive 

1858: literal $A$ in $GT_{G_0}$, $A\in N_{P^k}(\neg .TB_f^k)$

1859: if and only if all sub-derivations for $A$ 

1860: and $S$ (defined in Theorem \ref{main-th1}) 

1861: end with a failure leaf.

1862: \end{lemma}

1863: 

1864: \noindent {\bf Proof:}

1865: Let $GT_{G_0}^1=SLTP(P,G_0,R,\emptyset,\emptyset)$

1866: and $TB_t^1$ and $TB_f^1$ consist of all tabled positive and

1867: negative answers in $GT_{G_0}^1$, respectively. By Theorem \ref{main-th1},

1868: for any selected positive literal $A$ in $GT_{G_0}^1$, 

1869: $A\theta\in M_P(\emptyset)$ if and only if there is 

1870: a correct answer substitution for

1871: $A$ in $GT_{G_0}^1$ that is more general than $\theta$,

1872:  and that for any selected ground negative literal 

1873: $\neg A$ in $GT_{G_0}^1$, $A\in N_P(\emptyset)$

1874: if and only if all sub-derivations for $A$ in 

1875: $GT_{G_0}^1$ end with a failure leaf.

1876: Let $P^1=P\cup TB_t^1$. Then $P^1$ is equivalent to $P$ under the

1877: well-founded semantics.   

1878: 

1879: Let $GT_{G_0}^2=SLTP(P^1,G_0,R,TB_t^1,TB_f^1)$. Observe that 

1880: $SLTP(P^1,G_0,R,TB_t^1,$ $TB_f^1)$ works in the same way as 

1881: $SLTP(P^1,G_0,R,\emptyset,\emptyset)$ except whenever a negative

1882: subgoal $\neg A$ with $A\in TB_f^1$ is selected, it will directly be 

1883: treated as true instead of trying to prove $A$ by building a

1884: child SLT-tree $T_{\leftarrow A}$ for $\leftarrow A$. 

1885: When a positive subgoal $A\in TB_f^1$ is selected, 

1886: all sub-derivations for $A$ will still be generated.

1887: However, By Lemma \ref{sc-lem} all these sub-derivations

1888: will end with a failure leaf, which implies that $A$ is

1889: false. Therefore $SLTP(P^1,G_0,R,TB_t^1,TB_f^1)$

1890: can be viewed as $SLTP(P^1,G_0,R,\emptyset,\emptyset)$ with the 

1891: exception that all selected ground subgoals in $TB_f^1$ are 

1892: treated as false instead of being temporarily undefined. This means that

1893: $SLTP(P^1,G_0,R,TB_t^1,TB_f^1)$

1894: has the same relationship to $M_{P^1}(\neg .TB_f^1)$ and

1895: $N_{P^1}(\neg .TB_f^1)$ as $SLTP(P^1,G_0,R,\emptyset,\emptyset)$

1896: to $M_{P^1}(\emptyset)$ and $N_{P^1}(\emptyset)$. That is, by 

1897: Theorem \ref{main-th1} for any selected positive literal $A$ in $GT_{G_0}^2$, 

1898: $A\theta\in M_{P^1}(\neg .TB_f^1)$ if and only 

1899: if there is a correct answer substitution for

1900: $A$ in $GT_{G_0}^2$ that is more general than $\theta$, and 

1901: for any selected ground literal $A$ in $GT_{G_0}^2$, $A\in N_{P^1}(\neg .TB_f^1)$

1902: if and only if all sub-derivations for $A$ and

1903: $S$ in $GT_{G_0}^2$ end with a failure leaf. 

1904: 

1905: Continuing the above arguments, we will reach the same conclusion

1906: for any $GT_{G_0}^{i+1}=SLTP(P^i,G_0,R,TB_t^i,TB_f^i)$ 

1907: with $i\geq 1$. $\Box$

1908: 

1909: \vspace{4mm}

1910: 

1911: In the above proof we have $TB_f^1\subseteq N_P(\emptyset)$, so that

1912: $\neg .TB_f^1\subseteq WF(P)$. Meanwhile, for each $A\in TB_t^1$ we have

1913: $M_P(\emptyset)\models \forall (A)$, so that $WF(P) \models \forall (A)$.

1914: Therefore, $P^1=P\cup TB_t^1$ is equivalent to $P$ under the

1915: well-founded semantics, and by Lemma \ref{lem2-2} $M_{P^1}(\neg .TB_f^1)

1916: \subseteq WF(P)$ and $\neg .N_{P^1}(\neg .TB_f^1)\subseteq WF(P)$.

1917: For the same reason we have $TB_f^2\subseteq N_{P^1}(\neg .TB_f^1)$, so that

1918: $\neg .TB_f^2\subseteq WF(P)$; and for each $A\in TB_t^2$ we have

1919: $M_{P^1}(\neg .TB_f^1)\models \forall (A)$, so that $WF(P) \models \forall (A)$.

1920: This leads to $P^2=P\cup TB_t^2$ being equivalent to $P$ under the

1921: well-founded semantics, $M_{P^2}(\neg .TB_f^2)

1922: \subseteq WF(P)$ and $\neg .N_{P^2}(\neg .TB_f^2)\subseteq WF(P)$.

1923: Repeating this process leads to the following result.

1924: 

1925: \begin{corollary}

1926: \label{sc-cor2}

1927: For any $i\geq 1$, if $A\in TB_f^i$ then $WF(P)\models \neg A$,

1928: and if $A\in TB_t^i$ then $WF(P)\models \forall (A)$.

1929: \end{corollary}

1930: 

1931: \begin{lemma}

1932: \label{sc-lem3}

1933: $\qquad$

1934: \begin{enumerate}

1935: \item

1936: Let $A$ be a selected positive literal in $GT_{G_0}$.  

1937: For any (Herbrand) ground instance $A\theta$ of $A$, 

1938: $WF(P)\models A\theta$ if and only if $A\theta\in M_{P^k}(\neg .TB_f^k)$.

1939: \item

1940: For any selected ground negative literal $\neg A$ in $GT_{G_0}$,

1941: $WF(P)\models \neg A$ if and only if $A\in TB_f^k$.

1942: \end{enumerate}

1943: \end{lemma}

1944: 

1945: \noindent {\bf Proof:} 1. $(\Longleftarrow)$ Assume

1946: $A\theta\in M_{P^k}(\neg .TB_f^k)$. By Lemma \ref{sc-lem2} there 

1947: is a correct answer substitution for $A$ in $GT_{G_0}$ that is 

1948: more general than $\theta$. Since $TB_t^k$ consists of all tabled

1949: positive answers in all $GT_{G_0}^i$s $(i\geq 1)$, there is an

1950: $A\gamma\in TB_t^k$ with $\gamma$ more general than $\theta$.

1951: By Corollary \ref{sc-cor2} $WF(P)\models \forall (A\gamma)$, so that

1952: $WF(P)\models A\theta$.

1953: 

1954: $(\Longrightarrow)$ Assume $WF(P)\models A\theta$. Since $P^k$

1955: is equivalent to $P$ under the well-founded semantics, 

1956: $WF(P^k)\models A\theta$. Assume, on the contrary,

1957: $A\theta\not\in M_{P^k}(\neg .TB_f^k)$. Since $\neg .N_{P^k}(\neg 

1958: .TB_f^k)$ $\subseteq WF(P^k)$, $A\theta$ is in $O_{P^k}(\neg .TB_f^k)$.

1959: So there exists a ground backward chain of the form

1960: \begin{equation}

1961: \qquad A\theta\Rightarrow_{S_1}... \Rightarrow_{S_i}

1962: B_1,...,B_m,\neg D_1,...,\neg D_n\Rightarrow_{S_{i+1}}

1963: ...\Rightarrow_{S_t}\Box

1964: \qquad\qquad\qquad\qquad \label{chain2}

1965: \end{equation}

1966: where each step is performed by either resolving a positive literal

1967: like $B_j$ with an answer in $M_{P^k}(\neg .TB_f^k)$

1968: (when $B_j\in M_{P^k}(\neg .TB_f^k)$) or with 

1969: a Herbrand instantiated clause of $P$ (otherwise), 

1970: or removing a negative literal like

1971: $\neg D_j$ where $D_j\not\in M_{P^k}(\neg .TB_f^k)$. 

1972: Observe that for each negative literal

1973: $\neg D$ occurring in the chain, either $D\in TB_f^k$

1974: or $D\in O_{P^k}(\neg .TB_f^k)$ or $D\in N_{P^k}(\neg .TB_f^k)$.

1975: However, since $A\theta$ is true in $WF(P^k)$, $D$ must be false in $WF(P^k)$. 

1976: If $D$ is in $TB_f^k$, it has already been treated to be false; otherwise,  

1977: by Definition \ref{trans-ops2} $\neg D$ cannot be derived unless we 

1978: assume some atoms in $N_{P^k}(\neg .TB_f^k)-TB_f^k$ to be false. 

1979: This implies that for each negative literal $\neg D$ occurring in the 

1980: above chain with $D\not\in TB_f^k$, the proof of $D$ will be recursively

1981: reduced to the proof of some literals in $N_{P^k}(\neg .TB_f^k)-TB_f^k$. 

1982: 

1983: By using similar arguments of Theorem \ref{main-th1}, we can have

1984: a sub-derivation $SD_A$ for $A$ in $GT_{G_0}$, which corresponds to 

1985: the backward chain (\ref{chain2}), that ends with a temporarily undefined

1986: leaf. In $SD_A$, each selected ground negative 

1987: literal $\neg D$ is true if $D\in TB_f^k$; temporarily undefined, 

1988: otherwise (note $D\not\in M_{P^k}(\neg .TB_f^k)$). Since the sub-derivation

1989: ends with a temporarily undefined leaf, it has at least one 

1990: selected ground negative literal $\neg D$ with $D\not\in TB_f^k$.

1991: Let 

1992: \begin{center}

1993: $S=\{D|D\not\in TB_f^k$ and $\neg D$ is a selected ground negative

1994: literal in $SD_A$$\}$. 

1995: \end{center}

1996: Then by Lemma \ref{lem2-3} each $D\in S$ is either in 

1997: $N_{P^k}(\neg .TB_f^k)-TB_f^k$ 

1998: or in $O_{P^k}(\neg .TB_f^k)$. We consider two cases. 

1999: 

2000: Case 1. There exists a $D\in S$ with 

2001: $D\in N_{P^k}(\neg .TB_f^k)-TB_f^k$. 

2002: By Lemma \ref{sc-lem2} all sub-derivations for $D$ in $GT_{G_0}$ 

2003: end with a failure leaf. Since $D$ is not in $TB_f^k$, it is a 

2004: new tabled negative answer in $GT_{G_0}$, which contradicts that

2005: $GT_{G_0}$ has no new tabled negative answers.

2006: 

2007: Case 2. Every $D\in S$ is in $O_{P^k}(\neg .TB_f^k)$. 

2008: Since the backward chain (\ref{chain2}) is an instance of the

2009: sub-derivation $SD_A$, all $D$s in $S$ must be false in $WF(P^k)$.

2010: However, as discussed above no $\neg D$ can be derived unless we 

2011: assume some atoms in $N_{P^k}(\neg .TB_f^k)-TB_f^k$ to be false. That is,

2012: the proof of each $D\in S$ can be recursively

2013: reduced to the proof of some literals in $N_{P^k}(\neg .TB_f^k)-TB_f^k$.

2014: So $GT_{G_0}$ must have a subpath of the form 

2015: \begin{tabbing}

2016: $\qquad$ \= $...\neg D$\= $\ \cdots\triangleright$ $D\Rightarrow ...\Rightarrow$\\

2017: \>         $...\neg E_1$\> $\ \cdots\triangleright$ $E_1\Rightarrow ...\Rightarrow$\\

2018: \>\> $\quad \vdots$\\

2019: \>         $...\neg E_t$\> $\ \cdots\triangleright$ $E_t$

2020: \end{tabbing}

2021: \noindent where $E_t\in N_{P^k}(\neg .TB_f^k)-

2022: TB_f^k$. For the same reason as in the first case, $E_t$ should be

2023: a new tabled negative answer in $GT_{G_0}$, which leads to a contradiction. 

2024: 

2025: 2. $(\Longleftarrow)$ Immediate from Corollary \ref{sc-cor2}.

2026: 

2027: $(\Longrightarrow)$ Assume $WF(P)\models \neg A$ but on the

2028: contrary $A\not\in TB_f^k$. By point 1 of this lemma,

2029: $A\not\in M_{P^k}(\neg .TB_f^k)$. If $A\in N_{P^k}(\neg .TB_f^k)$ then

2030: by Lemma \ref{sc-lem2} all sub-derivations for $A$ in $GT_{G_0}$ will

2031: end with a failure leaf. Since $A$ is not in $TB_f^k$, it is a 

2032: new tabled negative answer, contradicting that

2033: $GT_{G_0}$ has no new tabled negative answers. 

2034: So $A\in O_{P^k}(\neg .TB_f^k)$.

2035: 

2036: Similar to the arguments for point 1 of this lemma, 

2037: the proof of $A$ can be recursively

2038: reduced to the proof of some literals in $N_{P^k}(\neg .TB_f^k)-

2039: TB_f^k$, which will lead to

2040: new tabled negative answers in $GT_{G_0}$, a contradiction. $\Box$

2041: 

2042: \begin{lemma}

2043: \label{sc-lem4}

2044: Let $G_0\leftarrow A$ be a top goal (with $A$ an atom). 

2045: $WF(P)\models \neg\exists (A)$ if and only if all branches of $T_{G_0}$

2046: end with a failure leaf.

2047: \end{lemma}

2048: 

2049: \noindent {\bf Proof:} 

2050: $(\Longleftarrow)$ Assume all branches of $T_{G_0}$ end with a failure

2051: leaf. Let $A\theta$ be a ground instance of $A$. By Lemmas \ref{sc-lem1}

2052: (point 2) and \ref{sc-lem2}, $A\theta\not\in M_{P^k}(\neg .TB_f^k)$,

2053: so by Lemma \ref{sc-lem3} $WF(P)\not\models A\theta$. Assume, on the 

2054: contrary, $WF(P)\not\models\neg A\theta$. By Corollary \ref{sc-cor2},

2055: $A\theta\not\in N_{P^k}(\neg .TB_f^k)$ and thus 

2056: $A\theta\in O_{P^k}(\neg .TB_f^k)$. Then there exists a ground 

2057: backward chain of the form

2058: \begin{equation}

2059: \qquad A\theta\Rightarrow_{S_1}... \Rightarrow_{S_i}

2060: B_1,...,B_m,\neg D_1,...,\neg D_n\Rightarrow_{S_{i+1}}

2061: ...\Rightarrow_{S_t}\Box

2062: \qquad\qquad\qquad\qquad \label{chain3}

2063: \end{equation}

2064: where each step is performed by either resolving a positive literal

2065: like $B_j$ with an answer in $M_{P^k}(\neg .TB_f^k)$

2066: (when $B_j\in M_{P^k}(\neg .TB_f^k)$) or with 

2067: a Herbrand instantiated clause of $P$ (otherwise), 

2068: or removing a negative literal like

2069: $\neg D_j$ where $D_j\not\in M_{P^k}(\neg .TB_f^k)$. 

2070: Observe that for each negative literal

2071: $\neg D$ occurring in the chain, either $D\in TB_f^k$

2072: or $D\in O_{P^k}(\neg .TB_f^k)$ or $D\in N_{P^k}(\neg .TB_f^k)$.

2073: However, since $A\theta$ is neither true nor false in $WF(P)$, 

2074: there exists at least one $D\in O_{P^k}(\neg .TB_f^k)$.

2075: 

2076: By using similar arguments of Theorem \ref{main-th1}, $T_{G_0}$ must have

2077: a branch, which corresponds to the backward chain (\ref{chain3}), 

2078: that ends with a temporarily undefined leaf. This contradicts the 

2079: assumption that all branches of $T_{G_0}$ end with a failure leaf.

2080: Therefore, for any ground instance $A\theta$ of $A$

2081: $WF(P)\models\neg A\theta$. That is, $WF(P)\models \neg\exists (A)$. 

2082: 

2083: $(\Longrightarrow)$ Assume $WF(P)\models \neg\exists (A)$. 

2084: By Lemmas \ref{sc-lem3} and \ref{sc-lem2}, there is no sub-derivation

2085: for $A$ that ends with a success leaf in $GT_{G_0}$.

2086: 

2087: Now assume, on the contrary, that $T_{G_0}$ has a branch $BR$ that

2088: ends with a temporarily undefined leaf. Then $BR$ has at least one

2089: ground instance corresponding to the ground backward chain like 

2090: (\ref{chain3}). Since $A\theta$ is false in $WF(P)$, there

2091: exists at least one ground negative literal $\neg D$ in the chain 

2092: such that $D$ is true in $WF(P)$. 

2093: This means that there is a selected ground negative literal $\neg D$

2094: in $BR$ such that $D$ is true in $WF(P)$. By Corollary \ref{sc-cor2}

2095: $D\not\in TB_f^k$, so by Definition \ref{slt-tree}

2096: a child SLT-tree $T_{\leftarrow D}$ must be

2097: built where $D$ is a selected positive literal. Since $BR$ is a

2098: temporarily undefined branch, $\neg D$ cannot fail, so

2099: $T_{\leftarrow D}$ has no successful branch (i.e. $\neg D$ is

2100: treated as $u^*$; see point 4 of Definition \ref{slt-tree}). 

2101: By Lemma \ref{sc-lem2} $D\not\in M_{P^k}(\neg .TB_f^k)$

2102: and by Lemma \ref{sc-lem3} $WF(P)\not\models D$, which contradicts 

2103: that $D$ is true in $WF(P)$. Therefore, all branches of $T_{G_0}$

2104: must end with a failure leaf. $\Box$

2105: 

2106: \vspace{4mm}

2107: 

2108: Now we are ready to show the

2109: soundness and completeness of SLT-resolution.

2110: 

2111: \begin{theorem}

2112: \label{sound-comp-normal}

2113: Let $\bar{P}$ be the augmented version of $P$.

2114: Let $G_0\leftarrow A$ be a top goal (with $A$ an atom) and

2115: $\theta$ a substitution for the variables of $A$. Assume 

2116: neither $A$ nor $\theta$ contains the 

2117: symbols $\bar{p}$ or $\bar{f}$ or $\bar{c}$.

2118: \begin{enumerate}

2119: \item

2120: $WF(P) \models \exists (A)$ if and only if $G_0$ is true 

2121: in $P$ with an instance of $A$;

2122: 

2123: \item

2124: $WF(P) \models \neg \exists (A)$ if and only if $G_0$ is false in $P$;

2125: 

2126: \item

2127: $WF(P) \not\models \exists (A)$ and  $WF(P) \not\models \neg\exists (A)$

2128: if and only if $G_0$ is undefined in $P$;

2129: 

2130: \item

2131: If $G_0$ is true in $P$ with an answer $A\theta$ then

2132: $WF(P) \models \forall (A\theta)$;

2133: 

2134: \item

2135: If $WF(\bar{P}) \models \forall (A\theta)$ then $G_0$ is true in $P$ with 

2136: an answer $A\theta$.

2137: \end{enumerate}

2138: \end{theorem}

2139: 

2140: \noindent {\bf Proof:} 

2141: \begin{enumerate}

2142: \item

2143: Immediate from Lemmas \ref{sc-lem2} and 

2144: \ref{sc-lem3}.

2145: 

2146: \item

2147: Immediate from Lemma \ref{sc-lem4}.

2148: 

2149: \item

2150: Immediate from points 1 and 2 of this theorem.

2151: 

2152: \item

2153: Assume $G_0$ is true in $P$ with an answer $A\theta$.

2154: Then there is a correct answer substitution $\gamma$ in $T_{G_0}$

2155: that is more general than $\theta$. By Theorem \ref{ans-subs}

2156: $WF(P^k) \models \forall (A\gamma)$ and thus

2157: $WF(P) \models \forall (A\gamma)$ since $P^k$ is equivalent to

2158: $P$ w.r.t. the well-founded semantics. Therefore

2159: $WF(P) \models \forall (A\theta)$.

2160: 

2161: \item

2162: Note that $\bar{P}=P\cup \{\bar{p}(\bar{f}(\bar{c}))\}$.

2163: Let $T_{G_0}'$ be the top SLT-tree in $GT_{G_0}'$ that 

2164: is returned by $SLT(\bar{P},G_0,R,\emptyset,\emptyset)$.

2165: Since none of the symbols $\bar{p}$ or $\bar{f}$ or $\bar{c}$

2166: appears in $P\cup \{G_0\}$, $T_{G_0}'=T_{G_0}$ and

2167: $GT_{G_0}'=GT_{G_0}$.

2168: 

2169: Let $\{X_0,...,X_n\}$ be the set of variables appearing

2170: in $A\theta$ and $\alpha$ be the ground substitution

2171: $\{X_0/\bar{c}, X_1/\bar{f}(\bar{c}),...,X_n/\bar{f}^n(\bar{c})\}$.

2172: Then $WF(\bar{P})\models A\theta\alpha$ and by Lemmas

2173: \ref{sc-lem3}, \ref{sc-lem2} and \ref{sc-lem1} 

2174: there is a correct answer substitution $\gamma$ for $G_0$ in 

2175: $T_{G_0}'$ that is more general than $\theta\alpha$. That is, there exists

2176: a substitution $\beta$ such that 

2177: $\gamma\beta=\theta\alpha$. Since $T_{G_0}'=T_{G_0}$,

2178: $\gamma$ contains neither $\bar{f}$ nor $\bar{c}$. So the only 

2179: occurrences of $\bar{f}$ and $\bar{c}$ in $\gamma\beta$

2180: are in $\beta$. Let $\beta'$ be obtained from $\beta$ by

2181: replacing every occurrence of $\bar{f}^i(\bar{c})$ by

2182: the variable $X_i$. Then $\gamma\beta'=\theta$ and thus

2183: $\gamma$ is more general than $\theta$. 

2184: 

2185: Since $T_{G_0}'=T_{G_0}$, there is a correct answer 

2186: substitution $\gamma$ for $G_0$ in 

2187: $T_{G_0}$ that is more general than $\theta$. Therefore,

2188: by Definition \ref{true-false} $G_0$ is true in $P$ with 

2189: an answer $A\theta$. $\Box$ 

2190: \end{enumerate}

2191: 

2192: Observe that in point 5 of Theorem \ref{sound-comp-normal}

2193: we used the augmented program $\bar{P}$ to characterize

2194: part of the completeness of SLT-resolution. The concept of

2195: augmented programs was introduced by Van Gelder, Ross

2196: and Schlipf \cite{VRS91}, which is used to deal with the so

2197: called {\em universal query problem} \cite{Prz89-2}.

2198: As indicated by Ross \cite{Ross92}, we cannot substitute

2199: $P$ for $\bar{P}$ in point 5 of Theorem \ref{sound-comp-normal}.

2200: A very simple illustrating example is that let $P=\{p(a)\}$ and

2201: $G_0=\leftarrow p(X)$, we have $WF(P)\models \forall (p(X)\{X/X\})$

2202: under Herbrand interpretations, but we have no correct answer

2203: substitution for $G_0$ in $T_{G_0}$ that is more general than

2204: $\{X/X\}$.

2205: 

2206: \section{Optimizations of SLT-resolution}

2207: \label{sec5}

2208: The objective of this paper

2209: is to develop an evaluation procedure for the well-founded

2210: semantics that is linear, free of infinite loops and with less redundant

2211: computations. Clearly, SLT-resolution is linear and with no infinite loops.

2212: However, like SLDNF-trees, SLT-trees defined in Definition 

2213: \ref{slt-tree} may contain a lot of duplicated

2214: sub-branches. SLT-resolution can be considerably optimized by eliminating

2215: those redundant computations. In this section we present three 

2216: effective methods for the optimization of SLT-resolution.

2217:  

2218: \subsection{Negation as the Finite Failure of Loop-Independent Nodes}

2219: From Definition \ref{slt} we see that SLT-resolution exhausts the

2220: answers of the top goal $G_0$ by recursively calling the function $SLTP()$.

2221: Obviously, the less the number of recursions is, the more efficient

2222: SLT-resolution would be. In this subsection we identify a large

2223: class of recursions that can easily be avoided. We start with an

2224: example.

2225: 

2226: \begin{example}

2227: \label{eg5-1}

2228: {\em

2229: Consider the following program:

2230: \begin{tabbing} 

2231: \hspace{.2in} $P_2$: \= $a \leftarrow \neg b.$ \`$C_{a_1}$ \\ 

2232: \> $b \leftarrow \neg c.$ \`$C_{b_1}$\\

2233: \> $c \leftarrow \neg d.$ \`$C_{c_1}$  

2234: \end{tabbing} 

2235: Let $G_0=\leftarrow a$ be the top goal. 

2236: Calling $SLT(P_2,G_0,R,\emptyset,\emptyset)$

2237: immediately invokes $SLTP(P_2,G_0,$ $R,\emptyset,\emptyset)$, which builds

2238: the first generalized SLT-tree $GT_{\leftarrow a}^1$

2239: as shown in Figure \ref{fig5-1} (a). Since there is no tabled positive 

2240: answer in $GT_{\leftarrow a}^1$ ($TB_t^1=\emptyset$), 

2241: the first tabled negative answer $d$ is 

2242: derived, which yields $TB_f^1=\{d\}$. Then 

2243: $SLT(P_2,G_0,R,\emptyset,TB_f^1)$ is called, which

2244: invokes $SLTP(P_2,G_0,R,\emptyset,TB_f^1)$ that builds the

2245: second generalized SLT-tree $GT_{\leftarrow a}^2$

2246: as shown in Figure \ref{fig5-1} (b). $GT_{\leftarrow a}^2$ has

2247: a new tabled positive answer $c$, so

2248: $SLTP(P_2\cup \{c\},G_0,R,\{c\},TB_f^1)$ is executed, which produces no

2249: new tabled positive answers. The second tabled negative

2250: answer $b$ is then obtained from $GT_{\leftarrow a}^2$. So far,

2251: $TB_t^2=\{c\}$ and $TB_f^2=\{b,d\}$. Next,

2252: $SLT(P_2\cup TB_t^2,G_0,R,TB_t^2,TB_f^2)$ is called, which

2253: invokes $SLTP(P_2\cup TB_t^2,G_0,R,TB_t^2,TB_f^2)$ that builds the

2254: third generalized SLT-tree $GT_{\leftarrow a}^3$

2255: as shown in Figure \ref{fig5-1} (c). We see $a$ is true in

2256: $GT_{\leftarrow a}^3$. As a result, to derive the first answer of $a$ 

2257: $SLT()$ is called three times and $SLTP()$ four times.

2258: 

2259: }

2260: \end{example}

2261: 

2262: \begin{figure}[htb]

2263: \centering

2264: 

2265: \setlength{\unitlength}{3947sp}%

2266: %

2267: \begingroup\makeatletter\ifx\SetFigFont\undefined%

2268: \gdef\SetFigFont#1#2#3#4#5{%

2269:   \reset@font\fontsize{#1}{#2pt}%

2270:   \fontfamily{#3}\fontseries{#4}\fontshape{#5}%

2271:   \selectfont}%

2272: \fi\endgroup%

2273: \begin{picture}(5325,3180)(226,-2611)

2274: \put(3151,-2611){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}(b) $GT_{\leftarrow a}^2$}}}

2275: \put(976,-2611){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}(a) $GT_{\leftarrow a}^1$}}}

2276: \put(5176,-961){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}(c) $GT_{\leftarrow a}^3$}}}

2277: \thinlines

2278: \put(1651,-436){\vector( 0,-1){200}}

2279: \put(1121,-1076){\vector(-2,-1){0}}

2280: \multiput(1501,-886)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

2281: \put(1051,-1336){\vector( 0,-1){200}}

2282: \put(596,-1976){\vector(-2,-1){0}}

2283: \multiput(976,-1786)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

2284: \put(2101,389){\vector( 0,-1){200}}

2285: \put(1646,-176){\vector(-2,-1){0}}

2286: \multiput(2026, 14)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

2287: \put(1051,-1786){\vector( 0,-1){200}}

2288: \put(1651,-886){\vector( 0,-1){200}}

2289: \put(2101,-11){\vector( 0,-1){200}}

2290: \put(3826,-436){\vector( 0,-1){200}}

2291: \put(3296,-1076){\vector(-2,-1){0}}

2292: \multiput(3676,-886)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

2293: \put(3226,-1336){\vector( 0,-1){200}}

2294: \put(4276,389){\vector( 0,-1){200}}

2295: \put(3821,-176){\vector(-2,-1){0}}

2296: \multiput(4201, 14)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

2297: \put(3226,-1736){\vector( 0,-1){200}}

2298: \put(4351,-11){\vector( 0,-1){200}}

2299: \put(5476,389){\vector( 0,-1){200}}

2300: \put(5476,-11){\vector( 0,-1){200}}

2301: \put(1426,-361){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_2:$ $ b$ }}}

2302: \put(1726,-586){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{b_1}$}}}

2303: \put(1276,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_3:$ $\neg c$ }}}

2304: \put(826,-1261){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_4:$ $c$ }}}

2305: \put(1126,-1486){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{c_1}$}}}

2306: \put(676,-1711){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_5:$ $\neg d$ }}}

2307: \put(226,-2236){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_6:$ $d$ }}}

2308: \put(451,-2086){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

2309: \put(1876,464){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_0:$ $a$ }}}

2310: \put(2176,314){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{a_1}$}}}

2311: \put(1726, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_1:$ $\neg b$ }}}

2312: \put(976,-2086){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_{u^*}$ }}}

2313: \put(901,-2236){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_7:$ $u^*$ }}}

2314: \put(2026,-361){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_{u^*}$ }}}

2315: \put(2026,-511){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_9:$ $u^*$ }}}

2316: \put(1576,-1186){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_{u^*}$ }}}

2317: \put(1501,-1336){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_8:$ $u^*$ }}}

2318: \put(3601,-361){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_2:$ $ b$ }}}

2319: \put(3901,-586){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{b_1}$}}}

2320: \put(3001,-1261){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_4:$ $c$ }}}

2321: \put(3301,-1486){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{c_1}$}}}

2322: \put(2851,-1711){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_5:$ $\neg d$ }}}

2323: \put(4051,464){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_0:$ $a$ }}}

2324: \put(4351,314){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{a_1}$}}}

2325: \put(3901, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_1:$ $\neg b$ }}}

2326: \put(3151,-2236){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_6:$  }}}

2327: \put(3151,-2086){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_t$}}}

2328: \put(3451,-886){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_3:$ $\neg c$ }}}

2329: \put(3751,-736){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

2330: \put(4201,-511){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_7:$ $u^*$ }}}

2331: \put(4276,-361){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_{u^*}$ }}}

2332: \put(3301,-1861){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$d\in TB_f^1$}}}

2333: \put(5251,464){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_0:$ $a$ }}}

2334: \put(5551,314){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{a_1}$}}}

2335: \put(5101, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_1:$ $\neg b$ }}}

2336: \put(5401,-361){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_t$ }}}

2337: \put(5326,-511){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_2:$  }}}

2338: \put(5551,-136){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$b\in TB_f^2$}}}

2339: \end{picture}

2340: 

2341: 

2342: \caption{The generalized SLT-trees $GT_{\leftarrow a}^1$, 

2343: $GT_{\leftarrow a}^2$ and $GT_{\leftarrow a}^3$.}\label{fig5-1}

2344: \end{figure} 

2345: 

2346: Carefully examining the generalized SLT-tree 

2347: $GT_{\leftarrow a}^1$ in Figure \ref{fig5-1},

2348: we notice that it contains no loops. That is, all nodes in it 

2349: are loop-independent. Consider the selected positive literal $d$

2350: at $N_6$. Since there is no sub-derivation for $d$ starting at $N_6$

2351: that ends with a temporarily undefined leaf and the proof of $d$

2352: is independent of all its ancestor subgoals, the set of sub-derivations

2353: for $d$ will remain unchanged throughout the recursions of $SLT()$;

2354: i.e. it will not change in all $GT_{\leftarrow a}^i$s $(i>1)$

2355: in which $d$ is a selected positive literal. This means that all answers

2356: of $d$ can be determined only based on its sub-derivations starting at 

2357: $N_6$ in $GT_{\leftarrow a}^1$, which leads to the following result. 

2358: 

2359: \begin{theorem}

2360: \label{th5-1}

2361: Let $GT_{G_0}=GT_{G_0}^{k+1}=SLTP(P^k,G_0,R,TB_t^k,TB_f^k)$, which

2362: is returned by $SLT(P,G_0,R,\emptyset,\emptyset)$.

2363: Let $A$ be a selected positive literal at a loop-independent node 

2364: $N_i$ in $GT_{G_0}^{j+1}=SLTP(P^j,G_0,R,TB_t^j,TB_f^j)$ $(j\leq k)$ 

2365: in which all sub-derivations $SD_A$

2366: for $A$ starting at $N_i$ end with a non-temporarily undefined leaf.

2367: Then $\theta$ is a correct answer substitution for $A$ in $SD_A$

2368: if and only if $A\theta$ is a tabled positive answer for $A$ in $TB_t^k$;

2369: and $A$ is false in $P$ if and only if all branches of $SD_A$ end with a failure

2370: leaf.

2371: \end{theorem}

2372: 

2373: \noindent {\bf Proof:}

2374: Let $T_{\leftarrow A}$ be the SLT-tree for $(P\cup \{\leftarrow A\},TB_f^j)$.

2375: Since $N_i$ is loop-independent, $SD_A=T_{\leftarrow A}$. Furthermore,

2376: since no branches in $T_{\leftarrow A}$ end with a temporarily

2377: undefined leaf, no new sub-derivations for $A$ will be generated

2378: via further recursions of $SLT()$. Therefore, in view of

2379: the fact that $TB_t^k$ consists of all

2380: tabled positive answers in all $GT_{G_0}^l$s,

2381: $\theta$ is a correct answer substitution for $A$ in $SD_A$

2382: if and only if $A\theta$ is a tabled positive answer for $A$ in $TB_t^k$. 

2383: And by Lemma \ref{sc-lem4}, $A$ is false in $P$ if and only if 

2384: all branches of $SD_A$ end with a failure leaf. $\Box$

2385: 

2386: \vspace{4mm}

2387: 

2388: Theorem \ref{th5-1} allows us to make the following enhancement

2389: of SLT-trees: 

2390: 

2391: \begin{optimization}

2392: \label{opt1}

2393: {\em

2394: In Definition \ref{slt-tree}

2395: change (c) of point 4 to (d) and add before it

2396: \begin{enumerate}

2397: \item[(c)]

2398: If the root of $T_{\leftarrow A}$ is loop-independent

2399: and all branches of $T_{\leftarrow A}$ end with a failure leaf

2400: then $N_i$ has only one child that is labeled

2401: by the goal $\leftarrow L_1,...,L_{j-1},L_{j+1},...,L_n$;

2402: \end{enumerate}

2403: }

2404: \end{optimization}

2405: 

2406: \begin{example}

2407: \label{eg5-2}

2408: {\em (Cont. of Example \ref{eg5-1})

2409: By applying the optimized algorithm for constructing 

2410: SLT-trees, SLT-resolution will build 

2411: the generalized SLT-tree $GT_{\leftarrow a}^1$

2412: as shown in Figure \ref{fig5-2}. Since $N_6$ is loop-independent,

2413: by Theorem \ref{th5-1} $d$ is false and thus $\neg d$ is true, 

2414: which leads to $c$ true and $\neg c$ false. Likewise, since

2415: $N_2$ is loop-independent, $b$ is false, which leads to

2416: $a$ true. As a result, to derive the first answer of $a$ 

2417: $SLT()$ is called ones and $SLTP()$ ones, which shows 

2418: a great improvement in efficiency over the former version.

2419: }

2420: \end{example}

2421: 

2422: \begin{figure}[htb]

2423: \centering

2424: 

2425: \setlength{\unitlength}{3947sp}%

2426: %

2427: \begingroup\makeatletter\ifx\SetFigFont\undefined%

2428: \gdef\SetFigFont#1#2#3#4#5{%

2429:   \reset@font\fontsize{#1}{#2pt}%

2430:   \fontfamily{#3}\fontseries{#4}\fontshape{#5}%

2431:   \selectfont}%

2432: \fi\endgroup%

2433: \begin{picture}(1950,2805)(226,-2236)

2434: \thinlines

2435: \put(1651,-436){\vector( 0,-1){200}}

2436: \put(1051,-1336){\vector( 0,-1){200}}

2437: \put(596,-1976){\vector(-2,-1){0}}

2438: \multiput(976,-1786)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

2439: \put(2101,389){\vector( 0,-1){200}}

2440: \put(1646,-176){\vector(-2,-1){0}}

2441: \multiput(2026, 14)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

2442: \put(1051,-1786){\vector( 0,-1){200}}

2443: \put(2101,-11){\vector( 0,-1){200}}

2444: \put(1046,-1101){\vector(-2,-1){0}}

2445: \multiput(1426,-911)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

2446: \put(1426,-361){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_2:$ $ b$ }}}

2447: \put(1726,-586){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{b_1}$}}}

2448: \put(826,-1261){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_4:$ $c$ }}}

2449: \put(1126,-1486){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{c_1}$}}}

2450: \put(676,-1711){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_5:$ $\neg d$ }}}

2451: \put(226,-2236){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_6:$ $d$ }}}

2452: \put(451,-2086){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

2453: \put(1876,464){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_0:$ $a$ }}}

2454: \put(2176,314){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{a_1}$}}}

2455: \put(1726, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_1:$ $\neg b$ }}}

2456: \put(976,-2086){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_t$ }}}

2457: \put(901,-2236){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_7:$ }}}

2458: \put(2026,-361){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_t$ }}}

2459: \put(2026,-511){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_8:$ }}}

2460: \put(1201,-886){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_3:$ $\neg c$ }}}

2461: \put(1576,-736){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

2462: \end{picture}

2463: 

2464: 

2465: \caption{The generalized SLT-tree $GT_{\leftarrow a}^1$ for 

2466: $(P_2\cup \{\leftarrow a\},\emptyset)$. $\qquad\qquad$}\label{fig5-2}

2467: \end{figure} 

2468: 

2469: It is easy to see that when the root of $T_{G_0}$ is loop-independent,

2470: $T_{G_0}$ is an SLDNF-tree and thus

2471: SLT-resolution coincides with SLDNF-resolution.

2472: Due to this reason, we call Optimization \ref{opt1}, which reduces

2473: recursions of $SLT()$, {\em negation as the finite 

2474: failure of loop-independent nodes.}

2475: 

2476: \subsection{Answer Completion}

2477: In this subsection we further optimize SLT-resolution 

2478: by implementing the intuition that

2479: if all answers of a positive literal $A$ have been derived and stored

2480: in the table $TB_t^i$ or $TB_f^i$ after the generation of

2481: $GT_{G_0}^i$, then all sub-derivations for $A$ in $GT_{G_0}^{i+1}$, which 

2482: are generated by applying program clauses

2483: (not tabled answers) to $A$, can be pruned because

2484: they produce no new answers for $A$. Again we begin with an example.

2485: 

2486: \begin{example}

2487: \label{eg5-3}

2488: {\em

2489: Let $P_3$ be $P_2$ of Example \ref{eg5-1} plus the program clause

2490: $C_{p_1}: p\leftarrow a,p$. Let $G_0=\leftarrow p$.

2491: SLT-resolution (with Optimization \ref{opt1}) first builds the generalized

2492: SLT-tree $GT_{G_0}^1$ as shown in Figure \ref{fig5-3} (a). Note that

2493: $N_1-N_7$ are loop-independent nodes, and $N_0$ and $N_9$

2494: are loop-dependent nodes. So $TB_t^1=\{c,a\}$ and 

2495: $TB_f^1=\{d,b\}$. Using these tabled answers SLT-resolution

2496: then builds the second generalized SLT-tree $GT_{G_0}^2$ as 

2497: shown in Figure \ref{fig5-3} (b). Since no new tabled positive answers 

2498: are generated in $GT_{G_0}^2$, $p$ is judged to be false.

2499: Hence $TB_t^2=TB_t^1=\{c,a\}$ and $TB_f^2=\{d,b,p\}$.

2500: Since $p$ is a new tabled negative answer, SLT-resolution

2501: starts a new recursion $SLT(P_3\cup TB_t^2, G_0,R,TB_t^2,TB_f^2)$, 

2502: which will build the third

2503: generalized SLT-tree $GT_{G_0}^3$ that is the same as $GT_{G_0}^2$.

2504: Since $GT_{G_0}^3$ contains no new tabled answers, the process stops.

2505: }

2506: \end{example}

2507: 

2508: \begin{figure}[htb]

2509: \centering

2510: 

2511: \setlength{\unitlength}{3947sp}%

2512: %

2513: \begingroup\makeatletter\ifx\SetFigFont\undefined%

2514: \gdef\SetFigFont#1#2#3#4#5{%

2515:   \reset@font\fontsize{#1}{#2pt}%

2516:   \fontfamily{#3}\fontseries{#4}\fontshape{#5}%

2517:   \selectfont}%

2518: \fi\endgroup%

2519: \begin{picture}(6847,3621)(526,-3436)

2520: \thicklines

2521: \multiput(4126,-1486)(75.00000,0.00000){12}{\makebox(6.6667,10.0000){\SetFigFont{10}{12}{\rmdefault}{\mddefault}{\updefault}.}}

2522: \multiput(4126,-436)(75.00000,0.00000){12}{\makebox(6.6667,10.0000){\SetFigFont{10}{12}{\rmdefault}{\mddefault}{\updefault}.}}

2523: \multiput(4126,-1486)(0.00000,70.00000){16}{\makebox(6.6667,10.0000){\SetFigFont{10}{12}{\rmdefault}{\mddefault}{\updefault}.}}

2524: \multiput(4951,-1486)(0.00000,70.00000){16}{\makebox(6.6667,10.0000){\SetFigFont{10}{12}{\rmdefault}{\mddefault}{\updefault}.}}

2525: \multiput(5551,-1486)(72.00000,0.00000){26}{\makebox(6.6667,10.0000){\SetFigFont{10}{12}{\rmdefault}{\mddefault}{\updefault}.}}

2526: \multiput(5551, 14)(72.00000,0.00000){26}{\makebox(6.6667,10.0000){\SetFigFont{10}{12}{\rmdefault}{\mddefault}{\updefault}.}}

2527: \multiput(5551,-1486)(0.00000,71.42857){22}{\makebox(6.6667,10.0000){\SetFigFont{10}{12}{\rmdefault}{\mddefault}{\updefault}.}}

2528: \multiput(7351,-1486)(0.00000,71.42857){22}{\makebox(6.6667,10.0000){\SetFigFont{10}{12}{\rmdefault}{\mddefault}{\updefault}.}}

2529: \put(1051,-3436){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}(a) $GT_{G_0}^1$}}}

2530: \put(3751,-1936){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}(b) $GT_{G_0}^2$}}}

2531: \put(6151,-1936){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}(c) $GT_{G_0}^3$}}}

2532: \thinlines

2533: \put(1351,-2161){\vector( 0,-1){200}}

2534: \put(1351,-2611){\vector( 0,-1){200}}

2535: \put(1951,-1261){\vector( 0,-1){200}}

2536: \put(2401,-436){\vector( 0,-1){200}}

2537: \put(1946,-1001){\vector(-2,-1){0}}

2538: \multiput(2326,-811)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

2539: \put(2401,-836){\vector( 0,-1){200}}

2540: \put(2401, 14){\vector( 0,-1){200}}

2541: \put(896,-2801){\vector(-2,-1){0}}

2542: \multiput(1276,-2611)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

2543: \put(4276,-436){\vector( 0,-1){200}}

2544: \put(4276,-836){\vector( 0,-1){200}}

2545: \put(4276, 14){\vector( 0,-1){200}}

2546: \put(4126,-386){\vector(-2,-1){380}}

2547: \put(6676,-436){\vector( 0,-1){200}}

2548: \put(6676,-836){\vector( 0,-1){200}}

2549: \put(6676, 14){\vector( 0,-1){200}}

2550: \put(6526,-386){\vector(-2,-1){380}}

2551: \put(1425,-1934){\vector(-2,-1){0}}

2552: \multiput(1805,-1744)(-63.33333,-31.66667){6}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}

2553: \put(1126,-2086){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_5:$ $c$ }}}

2554: \put(1426,-2311){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{c_1}$}}}

2555: \put(976,-2536){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_6:$ $\neg d$ }}}

2556: \put(526,-3061){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_7:$ $d$ }}}

2557: \put(751,-2911){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

2558: \put(1276,-2911){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_t$ }}}

2559: \put(1201,-3061){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_8:$ }}}

2560: \put(1501,-1711){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_4:$ $\neg c$ }}}

2561: \put(1876,-1561){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

2562: \put(1726,-1186){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_3:$ $ b$ }}}

2563: \put(2026,-1411){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{b_1}$}}}

2564: \put(2176,-361){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_1:$ $a,p$ }}}

2565: \put(2476,-511){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{a_1}$}}}

2566: \put(2026,-736){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_2:$ $\neg b,p$ }}}

2567: \put(2326,-1186){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$ }}}

2568: \put(2326,-1336){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_9:$ $p$ }}}

2569: \put(2176, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_0:$ $p$ }}}

2570: \put(2476,-136){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{p_1}$}}}

2571: \put(4201,-1186){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$ }}}

2572: \put(4051, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_0:$ $p$ }}}

2573: \put(4351,-586){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{a_1}$}}}

2574: \put(4201,-1336){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_4:$ $p$ }}}

2575: \put(4351,-136){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{p_1}$}}}

2576: \put(3226,-511){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$a\in TB_t^1$}}}

2577: \put(4201,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_3:$ $\neg b,p$ }}}

2578: \put(3976,-361){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_1:$ $a,p$ }}}

2579: \put(3676,-736){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$ }}}

2580: \put(3526,-886){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_2:$ $p$ }}}

2581: \put(6601,-1186){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$ }}}

2582: \put(6451, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_0:$ $p$ }}}

2583: \put(6751,-586){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{a_1}$}}}

2584: \put(6601,-1336){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_4:$ $p$ }}}

2585: \put(6751,-136){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{p_1}$}}}

2586: \put(5626,-511){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$a\in TB_t^1$}}}

2587: \put(6601,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_3:$ $\neg b,p$ }}}

2588: \put(6376,-361){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_1:$ $a,p$ }}}

2589: \put(6076,-736){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$ }}}

2590: \put(5926,-886){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_2:$ $p$ }}}

2591: \put(4351,-1036){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$b\in TB_f^1$}}}

2592: \put(6751,-1036){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$b\in TB_f^1$}}}

2593: \end{picture}

2594: 

2595: 

2596: \caption{The generalized SLT-trees $GT_{G_0}^1$, $GT_{G_0}^2$

2597: and $GT_{G_0}^3$. $\qquad\qquad$}\label{fig5-3}

2598: \end{figure} 

2599: 

2600: Examining $GT_{G_0}^2$ in Figure \ref{fig5-3} we observe that since by

2601: Theorem \ref{th5-1} all answers of $a$ have already been stored in $TB_t^1$, 

2602: the sub-derivation for $a$ via the clause $C_{a_1}$ (circumscribed by

2603: the dotted box) is redundant and hence can be removed. Similarly,

2604: since the unique answer of $p$ has already been stored in $TB_f^2$, the 

2605: circumscribed sub-derivations for $p$ via the clause $C_{p_1}$ in $GT_{G_0}^3$

2606: are redundant and thus can be removed. We now discuss how to 

2607: realize such type of optimization. 

2608: 

2609: First, we associate with each

2610: selected positive literal $A$ (or its variant) a {\em completion}

2611: flag $comp(A)$, defined by

2612: 

2613: \[comp(A)=\left\{\begin{array}{ll}

2614:           Yes  & \mbox{if the answers of $A$ are completed;}\\

2615:           No   & \mbox{otherwise.}

2616:                  \end{array}

2617:           \right. \] 

2618: 

2619: \noindent We say the answers of $A$ are {\em completed} if all its

2620: answers have been stored in some $TB_t^i$ or $TB_f^i$. 

2621: The determination of whether a selected positive literal

2622: $A$ has got its complete answers is based on

2623: Theorem \ref{th5-1}. That is, for a

2624: selected positive literal $A$ at node $N_k$, $comp(A)=Yes$ if 

2625: $N_k$ is loop-independent (assume Optimization \ref{opt1}

2626: has already been applied). In addition, for each tabled negative answer 

2627: $A$ in $TB_f^i$, $comp(A)$ should be $Yes$. 

2628: 

2629: Then, before applying program clauses to a selected

2630: positive literal $A$ as in point 3 of Definition \ref{slt-tree},

2631: we do the following:

2632: 

2633: \begin{optimization}

2634: \label{opt2}

2635: {\em

2636: Check the flag $comp(A)$. If it is $Yes$ then apply to $A$ no program clauses

2637: but tabled answers. 

2638: }

2639: \end{optimization}

2640: 

2641: \begin{example}

2642: {\em (Cont. of Example \ref{eg5-3})

2643: Based on $GT_{G_0}^1$ in Figure \ref{fig5-3}, $comp(a)$, $comp(b)$,

2644: $comp(c)$ and $comp(d)$ will be set to $Yes$ since

2645: $N_1$, $N_3$, $N_5$ and $N_7$ are loop-independent.

2646: Therefore, the circumscribed sub-derivation in $GT_{G_0}^2$ will 

2647: not be generated by the optimized SLT-resolution. 

2648: Likewise, although $N_0:p$ in $GT_{G_0}^2$ is loop-dependent,

2649: once $p$ is added to $TB_f^2$, $comp(p)$ will be set to $Yes$.

2650: As a result, the circumscribed sub-derivations in $GT_{G_0}^3$

2651: will never occur, so that $GT_{G_0}^3$ will consist only of a single

2652: failure leaf at its root.

2653: }

2654: \end{example}

2655: 

2656: \subsection{Eliminating Duplicated Sub-Branches 

2657: Based on a Fixed Depth-First Control Strategy}

2658: \label{sec-dup}

2659: Consider two selected positive literals $A_1$ at 

2660: node $N_1$ and $A_2$ at node $N_2$ in

2661: $GT_{G_0}^i$ such that $A_1$ is a variant of $A_2$.

2662: Let $\{C_1,...,C_m\}$ be the set of program clauses in $P$ 

2663: whose heads can unify with $A_1$. Then both $A_1$ and $A_2$ will

2664: use all the $C_j$s except for looping clauses. This introduces

2665: obvious redundant sub-branches, starting at $N_1$ and $N_2$ respectively. 

2666: In this subsection we optimize SLT-resolution by eliminating this type of

2667: redundant computations. We begin by making

2668: the following two simple and yet practical assumptions.

2669: \begin{enumerate}

2670: \item

2671: We assume that program clauses and tabled answers are

2672: stored separately, and that new intermediate answers in SLT-trees 

2673: are added into their tables once they are generated (i.e. new tabled 

2674: positive answers are collected during the construction of each $GT_{G_0}^i$).

2675: All tabled answers can be used once they are added to tables.

2676: For instance, in Figure \ref{fig5-2} the intermediate answer $c$ is added to

2677: the table $TB_t$ right after node $N_7$ is generated. Such an answer

2678: can then be used thereafter. Obviously, this assumption does

2679: not affect the correctness of SLT-resolution.

2680: \item 

2681: We assume nodes in each $GT_{G_0}^i$ are generated 

2682: one after another in an order specified by a depth-first control strategy.

2683: A {\em control strategy} consists of a search rule, a computation rule,

2684: and policies for selecting program clauses and tabled answers.

2685: A {\em search rule} is a rule for selecting a node among all nodes

2686: in a generalized SLT-tree. A {\em depth-first} search rule is a 

2687: search rule that starting from the root node always selects the most 

2688: recently generated node. Depth-first rules are the most widely used search rules in

2689: artificial intelligence and programming languages because they can

2690: be very efficiently implemented using a simple stack-based memory structure.

2691: For this reason, in this paper we choose depth-first control strategies,

2692: i.e. control strategies with a depth-first search rule.

2693: \end{enumerate}

2694: 

2695: The intuitive idea behind the optimization is that after a clause

2696: $C_j$ has been completely used by $A_1$ at $N_1$, 

2697: it needs not be used by $A_2$ at $N_2$. 

2698: We describe how to achieve this.

2699: 

2700: Let $CS$ be a depth-first control strategy and assume $A_1$ 

2701: at $N_1$ is currently selected by $CS$. 

2702: Instead of generating all child nodes of $N_1$

2703: by simultaneously applying to $A_1$ all 

2704: program clauses and tabled answers (as in point 3

2705: of Definition \ref{slt-tree}), each time only one clause or tabled answer, say

2706: $C_j$, is selected by $CS$ to apply to $A_1$. This yields one child node,

2707: say $N_s$. Then $N_s$ will be immediately expanded in the same way (recursively) since

2708: it is the most recently generated node. 

2709: After the expansion of $N_s$ has been finished, its parent node

2710: $N_1$ is selected again by $CS$ (since it is 

2711: the most recently generated node among all unfinished nodes) and expanded

2712: by applying to $A_1$ another clause or tabled answer (selected by $CS$). 

2713: If no new clause or tabled answer is left for $A_1$, which means that 

2714: all sub-branches starting at $N_1$ in $GT_{G_0}^i$

2715: have been exhausted, the expansion of $N_1$ is finished.

2716: The control is then back to the parent node of $N_1$.

2717: This process is usually called {\em backtracking}.

2718: Continue this way until we finish the expansion of the root node

2719: of $GT_{G_0}^i$. Since $GT_{G_0}^i$ is finite (for programs with the bounded-term-size

2720: property), $CS$ is {\em complete} for SLT-resolution in the sense

2721: that all nodes of $GT_{G_0}^i$ will be generated using this control strategy.

2722: This shows a significant advantage over SLDNF-resolution, which

2723: is incomplete with a depth-first control strategy because of possible

2724: infinite loops in SLDNF-trees \cite{Ld87}. Moreover, the above description

2725: clearly demonstrates that SLT-resolution is linear for query evaluation.

2726: 

2727: In the above description, when backtracking to $N_1$ from $N_s$, 

2728: all sub-branches starting at $N_1$ via $C_j$ in $GT_{G_0}^i$ must

2729: have been exhausted. In this case, we say $C_j$ {\em has been completely

2730: used} by $A_1$. For each program clause $C_j$

2731: whose head can unify with $A_1$, we associate with $A_1$ (or its variant) 

2732: a flag $comp\_used(A_1,C_j)$, defined by  

2733: 

2734: \[comp\_used(A_1,C_j)=\left\{\begin{array}{ll}

2735:           Yes  & \mbox{if $C_j$ has been completely used by $A_1$ (or its variant);}\\

2736:           No   & \mbox{otherwise.}

2737:                  \end{array}

2738:           \right. \] 

2739: 

2740: From the above description we see that given a fixed depth-first

2741: control strategy, program clauses will be selected and applied

2742: in a fixed order. Therefore, by the time $C_j$ is selected for $A_2$ at $N_2$,

2743: we check the flag $comp\_used(A_2,C_j)$. 

2744: If $comp\_used(A_2,C_j)=Yes$ then $C_j$ needs not be applied to $A_2$

2745: since similar sub-derivations have been completed before with all

2746: intermediate answers along these sub-derivations already stored in tables 

2747: for $A_2$ to use (under the above first assumption).

2748: 

2749: Observe that in addition to deriving new answers, the application of 

2750: $C_j$ to $A_1$ may change the property of loop dependency of $N_1$,

2751: which is important to Optimizations \ref{opt1} and \ref{opt2}.

2752: That is, if some sub-branch starting at $N_1$ via $C_j$ contains

2753: loop nodes then $N_1$ will be loop-dependent. If $N_1$ is loop-dependent,

2754: neither Optimization \ref{opt1} nor Optimization \ref{opt2} is

2755: applicable, so the answers of $A_1$ can be completed only through

2756: the recursions of SLT-resolution. Since $A_2$ is a variant

2757: of $A_1$, $N_2$ should have the same property as $N_1$. To achieve this,

2758: we associate with $A_1$ (or its variant) a

2759: flag $loop\_depend(A_1)$, defined by

2760: 

2761: \[loop\_depend(A_1)=\left\{\begin{array}{ll}

2762:           Yes  & \mbox{if $A_1$ (or its variant)

2763:                  has been selected at some} \\

2764:               &  \mbox{loop-dependent node;}\\

2765:           No   & \mbox{otherwise.}

2766:                  \end{array}

2767:           \right. \]

2768: Then at node $N_2$ we check the flag.

2769: If $loop\_depend(A_2)=Yes$ then mark $N_2$ as a loop node, 

2770: so that $N_2$ becomes loop-dependent.

2771:  

2772: To sum up, SLT-trees can be generated using a fixed depth-first  

2773: control strategy $CS$, where the following mechanism is used for selecting

2774: program clauses (not tabled answers):

2775: 

2776: \begin{optimization}

2777: \label{opt3}

2778: {\em 

2779: Let $A$ be the currently selected

2780: positive literal at node $N_k$. If $loop\_depend(A)$ $=Yes$, 

2781: mark $N_k$ as a loop node. A clause $C_j$ is selected for $A$

2782: based on $CS$ such that $C_j$ is not a looping clause of $A$ and

2783: $comp\_used(A,C_j)=No$.

2784: }

2785: \end{optimization}

2786: 

2787: \begin{theorem}

2788: \label{th5-2}

2789: Optimization \ref{opt3} is correct.

2790: \end{theorem}

2791: 

2792: \noindent {\bf Proof:} The exclusion of looping clauses has been

2793: justified in SLT-resolution before. Here we justify the exclusion

2794: of program clauses that have been completely used.

2795: Let $A_1$ at node $N_1$ and $A_2$ at node $N_2$

2796: be two variant subgoals in $GT_{G_0}^i$ and let $C_j$ have been completely 

2797: used by $A_1$ by the time $C_j$ is selected for $A_2$. 

2798: Since we use a fixed depth-first control strategy, 

2799: all sub-derivations for $A_1$ via $C_j$ must have been

2800: generated, independently of applying $C_j$ to $A_2$.

2801: This means that applying $C_j$ to $A_2$ will generate similar 

2802: sub-derivations. Thus skipping $C_j$ at $N_2$ will not lose

2803: any answers to $A_2$ provided that $A_2$ has access to the answers

2804: of $A_1$ and that $N_2$ has the same property of loop dependency

2805: as $N_1$. Clearly, that $N_2$ has the same property of loop dependency

2806: as $N_1$ is guaranteed by using the flag $loop\_depend(A_1)$, and

2807: the access of $A_2$ to the answers of $A_1$ is achieved by

2808: the first assumption above. 

2809: 

2810: Observe that the application of

2811: the first assumption may lead to more sub-derivations for $A_2$ via 

2812: $C_j$ than those for $A_1$ via $C_j$. These extra sub-branches are

2813: generated by using some newly added tabled answers, $S_1$, during

2814: the construction of $GT_{G_0}^i$, which

2815: were not yet available during the generation of sub-derivations of 

2816: $A_1$ via $C_j$. If these extra sub-branches would yield new tabled answers, $S_2$,

2817: the sub-derivations of $A_1$ via $C_j$ must have a loop. In this case, 

2818: however, the newly added tabled answers $S_1$ will be

2819: applied to the generation of sub-derivations of $A_1$ via $C_j$ in the

2820: next recursion of SLT-resolution, which produces similar sub-branches

2821: with new tabled answers $S_2$. Since $A_2$ is loop-dependent as $A_1$, it will be

2822: generated in this recursion and use the answers $S_2$ from $A_1$.

2823: $\Box$

2824: 

2825: \vspace{4mm}

2826: 

2827: The following two results show that redundant applications of

2828: program clauses to variant subgoals are reduced by 

2829: Optimization \ref{opt3}.

2830: 

2831: \begin{theorem}

2832: \label{th5-3}

2833: Let $A_1$ at node $N_1$ be an ancestor variant subgoal of $A_2$ at node $N_2$.

2834: The program clauses used by the two subgoals are disjoint.

2835: \end{theorem}

2836: 

2837: \noindent {\bf Proof:} Let $CS$ be a fixed depth-first control strategy

2838: and $\{C_1,...,C_m\}$ be the set

2839: of program clauses whose heads can unify with $A_1$. Assume these clauses 

2840: are selected by $CS$ sequentially from left to right.

2841: Since $A_1$ at $N_1$ is an ancestor variant of $A_2$ at $N_2$,

2842: let $C_i$ be the clause via which the sub-branch starting at 

2843: $N_1$ leads to $N_2$. Obviously, $C_i$ will not be used by $A_2$

2844: since it is a looping clause of $A_2$. 

2845: 

2846: By Optimization \ref{opt3},

2847: for each $1\leq j<i$ by the time $t$ when $C_i$ was selected for $A_1$ at $N_1$,

2848: $C_j$ is either a looping clause of $A_1$ or $comp\_used(A_1,C_j)=Yes$.

2849: Since $N_2$ was generated after $t$,  

2850: $C_j$ is either a looping clause of $A_2$ or $comp\_used(A_2,C_j)=Yes$.

2851: So $C_j$ will not be used by $A_2$ at $N_2$. 

2852: 

2853: Since $CS$ adopts a depth-first search rule,

2854: by the time $t_1$ when $A_1$ tries to select the next clause $C_k$ $(k>i)$

2855: $C_i$ must have been completely used by $A_1$ (via backtracking).

2856: This implies that all $C_j$s $(i< j\leq m)$ must have been

2857: completely used before $t_1$ by $A_2$. Hence

2858: for no $i< j\leq m$ $C_j$ will be available to $A_1$. $\Box$

2859: 

2860: \begin{theorem}

2861: \label{th5-4}

2862: Let $A_1=p(.)$ and $C_{p_j}$ be a program clause whose head can unify

2863: with $A_1$. Assume the number of tabled answers of $A_1$ is bounded by $N$.

2864: Then $C_{p_j}$ is applied in $GT_{G_0}^i$ by $O(N)$ variant subgoals 

2865: of $A_1$.

2866: \end{theorem}

2867: 

2868: \noindent {\bf Proof:}

2869: Let $\{A_1,...,A_m\}$ be the set of variant subgoals that are selected

2870: in $GT_{G_0}^i$. The worst case is like this: The application of $C_{p_j}$

2871: to $A_1$ yields the first tabled answer of $A_1$, but $C_{p_j}$ has not yet

2872: been completely used after this. Next $A_2$ is selected, which uses the first

2873: tabled answer and then applies $C_{p_j}$ to produce the second tabled

2874: answer. Again $C_{p_j}$ has not yet been completely used after this.

2875: Continue this way until $A_{N+1}$ is selected, which uses all the $N$

2876: tabled answers and then applies $C_{p_j}$. This time it will fail to

2877: produce any new tabled answer after exhausting all the remaining 

2878: branches of $A_{N+1}$ via $C_{p_j}$. So $C_{p_j}$

2879: has been completely used by $A_{N+1}$ and the flag $comp\_used(A_{N+1},C_{p_j})$

2880: is set to $Yes$. Therefore $C_{p_j}$ will never be applied to any selected

2881: variant subgoals of $A_1$ thereafter. $\Box$

2882: 

2883: \begin{example}

2884: \label{dsz}

2885: {\em

2886: Consider the following program and let $G_0=\leftarrow p(X,5)$ be the 

2887: top goal.\footnote{This program is suggested by B. Demon, K. Sagonas and N. F. Zhou.}

2888: \begin{tabbing} 

2889: \hspace{.2in} $P_3$: \= 

2890: $p(X,N)\leftarrow loop(N),p(Y,N),odd(Y),X$ is $Y+1,X<N.$ \`$C_{p_1}$ \\

2891: \> $p(X,N)\leftarrow p(Y,N),even(Y),X$ is $Y+1,X<N.$ \`$C_{p_2}$ \\

2892: \> $p(1,N).$ \`$C_{p_3}$\\

2893: \> $loop(N).$ \`$C_{l_1}$ 

2894: \end{tabbing}

2895: Here, $odd(Y)$ is true if $Y$ is an odd number, and 

2896: $even(Y)$ is true if $Y$ is an even number.`` $X$ is $Y+1$'' is 

2897: a meta-predicate which computes $Y+1$ and then assigns the 

2898: result to $X$. 

2899: 

2900: We assume using the Prolog control strategy:

2901: depth-first for node/goal selection + 

2902: left-most for subgoal selection

2903: + top-down for clause selection. Obviously, it is a 

2904: depth-first control strategy. We also assume using the 

2905: first-in-first-out policy for selecting answers in tables.

2906: If both program clauses and tabled answers are available,

2907: tabled answers are used first. Let $CS$ represent the whole

2908: control strategy. Then SLT-resolution (enhanced with 

2909: Optimization \ref{opt3}) evaluates $G_0$ step by step and

2910: generates a sequence of nodes $N_0,$ $N_1,$ $N_2,$ and so on, as shown in

2911: Figures \ref{fig5-4} and \ref{fig5-5}.

2912: 

2913: 

2914: \begin{figure}[htb]

2915: %\centering

2916: 

2917: \setlength{\unitlength}{3947sp}%

2918: %

2919: \begingroup\makeatletter\ifx\SetFigFont\undefined%

2920: \gdef\SetFigFont#1#2#3#4#5{%

2921:   \reset@font\fontsize{#1}{#2pt}%

2922:   \fontfamily{#3}\fontseries{#4}\fontshape{#5}%

2923:   \selectfont}%

2924: \fi\endgroup%

2925: \begin{picture}(5862,2871)(2476,-2536)

2926: \thinlines

2927: \put(6676,-1711){\vector( 0,-1){225}}

2928: \put(6676,-1186){\vector( 0,-1){225}}

2929: \put(7651,164){\vector( 3,-1){675}}

2930: \put(6676,-736){\vector( 0,-1){225}}

2931: \put(6676,-286){\vector( 0,-1){225}}

2932: \put(6676,164){\vector(-3,-1){675}}

2933: \put(6676,-2161){\vector( 0,-1){225}}

2934: \put(7726,-736){\vector( 4,-1){300}}

2935: \put(5176,-736){\vector(-4,-1){600}}

2936: \put(3751,-1411){\vector( 0,-1){225}}

2937: \put(6751,-1861){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$X=2$}}}

2938: \put(6751,-2236){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}Add $p(2,5)$ to $TB_t^1$}}}

2939: \put(6751,-886){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$p(1,5)$}}}

2940: \put(6076,-1636){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_6:$  $X$ is $1+1,X<5$}}}

2941: \put(6451,-2086){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_7:$  $2<5$}}}

2942: \put(4276,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$C_{p_2}$}}}

2943: \put(6076, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$C_{p_1}$}}}

2944: \put(8101, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$p(1,5)$}}}

2945: \put(6751,-436){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$C_{l_1}$}}}

2946: \put(6376,-2536){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_8:$   $\Box_t$}}}

2947: \put(2476,-1111){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_3:$  $p(Y_1,5),even(Y_1),Y$ is $Y_1+1,Y<5,$}}}

2948: \put(5626,-1111){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_5:$  $odd(1),X$ is $1+1,X<5$}}}

2949: \put(7801,-1111){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_9:$  $odd(2),X$ is $2+1,X<5$}}}

2950: \put(3976,-211){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_1:$  $loop(5),p(Y,5),odd(Y),X$ is $Y+1,X<5$}}}

2951: \put(5176,-661){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_2:$  $p(Y,5),odd(Y),X$ is $Y+1,X<5$}}}

2952: \put(8101,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$p(2,5)$}}}

2953: \put(8101,-211){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{10}:$   $\Box_t$}}}

2954: \put(8101,-961){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

2955: \put(3076,-1336){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$odd(Y),X$ is $Y+1,X<5$}}}

2956: \put(2626,-1936){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_4:$  $even(1),Y$ is $1+1,Y<5,$}}}

2957: \put(3001,-2161){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$odd(Y),X$ is $Y+1,X<5$}}}

2958: \put(3451,-1561){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$C_{p_3}$}}}

2959: \put(3826,-1561){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}Add $p(1,5)$ to $TB_t^1$}}}

2960: \put(3676,-1786){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

2961: \put(6751,239){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_0:$ $p(X,5)$ }}}

2962: \end{picture}

2963: 

2964: 

2965: \caption{$GT_{G_0}^1$. $\qquad\qquad\qquad\qquad\qquad$}\label{fig5-4}

2966: \end{figure}

2967: 

2968: 

2969: \begin{figure}

2970: %\centering

2971: 

2972: 

2973: \setlength{\unitlength}{3947sp}%

2974: %

2975: \begingroup\makeatletter\ifx\SetFigFont\undefined%

2976: \gdef\SetFigFont#1#2#3#4#5{%

2977:   \reset@font\fontsize{#1}{#2pt}%

2978:   \fontfamily{#3}\fontseries{#4}\fontshape{#5}%

2979:   \selectfont}%

2980: \fi\endgroup%

2981: \begin{picture}(6225,7596)(3001,-6886)

2982: \thinlines

2983: \put(6301,389){\vector( 0,-1){225}}

2984: \put(4426,389){\vector( 0,-1){225}}

2985: \put(3601,389){\vector( 0,-1){225}}

2986: \put(8626,389){\vector( 0,-1){225}}

2987: \put(3601,389){\line( 1, 0){5025}}

2988: \put(6301,-61){\vector( 0,-1){225}}

2989: \put(6301,-661){\vector( 0,-1){225}}

2990: \put(7951,-1861){\vector( 0,-1){225}}

2991: \put(7951,-1336){\vector( 0,-1){225}}

2992: \put(7951,-2311){\vector( 0,-1){225}}

2993: \put(3601,-1861){\vector( 0,-1){225}}

2994: \put(3601,-1336){\vector( 0,-1){225}}

2995: \put(3601,-2311){\vector( 0,-1){225}}

2996: \put(3676,-661){\line( 1, 0){5475}}

2997: \put(6301,-661){\line( 0, 1){150}}

2998: \put(3676,-661){\vector( 0,-1){225}}

2999: \put(7951,-661){\vector( 0,-1){225}}

3000: \put(4876,-661){\vector( 0,-1){225}}

3001: \put(9151,-661){\vector( 0,-1){225}}

3002: \put(6301,-1561){\line( 0,-1){1350}}

3003: \put(4651,-3961){\vector( 0,-1){225}}

3004: \put(4651,-4636){\vector( 0,-1){225}}

3005: \put(4651,-5086){\vector( 0,-1){225}}

3006: \put(4651,-6061){\vector( 0,-1){225}}

3007: \put(4651,-5536){\vector( 0,-1){225}}

3008: \put(4651,-6511){\vector( 0,-1){225}}

3009: \put(7726,-3961){\vector( 0,-1){225}}

3010: \put(7726,-4636){\vector( 0,-1){225}}

3011: \put(3376,-2911){\line( 1, 0){5700}}

3012: \put(3376,-2911){\vector( 0,-1){225}}

3013: \put(6301,-2911){\vector( 0,-1){225}}

3014: \put(9076,-2911){\vector( 0,-1){225}}

3015: \put(4726,-2911){\vector( 0,-1){375}}

3016: \put(7801,-2911){\vector( 0,-1){375}}

3017: \put(6301,539){\line( 0,-1){150}}

3018: \put(3151,239){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$p(1,5)$}}}

3019: \put(4051,239){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$p(2,5)$}}}

3020: \put(6001,239){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$C_{p_1}$}}}

3021: \put(8251, 14){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{29}:$   $\Box_t$}}}

3022: \put(8701,239){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$p(3,5)$}}}

3023: \put(5701,-1036){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{10}:$  $p(Y_1,5),even(Y_1),$}}}

3024: \put(7651,-1036){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{24}:$  $odd(3),$}}}

3025: \put(8026,-2011){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$X=4$}}}

3026: \put(7351,-1786){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{25}:$  $X$ is $3+1,X<5$}}}

3027: \put(7726,-2236){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{26}:$  $4<5$}}}

3028: \put(7651,-2686){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{27}:$   $\Box_t$}}}

3029: \put(3301,-1036){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_5:$  $odd(1),$}}}

3030: \put(3676,-2011){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$X=2$}}}

3031: \put(3001,-1786){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_6:$  $X$ is $1+1,X<5$}}}

3032: \put(3376,-2236){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_7:$  $2<5$}}}

3033: \put(3301,-2686){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_8:$   $\Box_t$}}}

3034: \put(3076,-1261){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$X$ is $1+1,X<5$}}}

3035: \put(3226,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$p(1,5)$}}}

3036: \put(5926,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$C_{p_2}$}}}

3037: \put(7576,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$p(3,5)$}}}

3038: \put(5851,-1261){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$Y$ is $Y_1+1,Y<5,$}}}

3039: \put(5551,-1486){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$odd(Y),X$ is $Y+1,X<5$}}}

3040: \put(7501,-1261){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$X$ is $3+1,X<5$}}}

3041: \put(4426,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$p(2,5)$}}}

3042: \put(4426,-1111){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_9:$  $odd(2),...$}}}

3043: \put(4801,-961){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

3044: \put(8776,-1111){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{28}:$  $odd(4),...$}}}

3045: \put(9076,-961){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

3046: \put(5701,-3436){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{19}:$  $even(3),...$}}}

3047: \put(3001,-3436){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{11}:$  $even(1),...$}}}

3048: \put(4276,-3436){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{12}:$  $even(2),$}}}

3049: \put(4051,-3661){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$Y$ is $2+1,Y<5,$}}}

3050: \put(4726,-6211){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$X=4$}}}

3051: \put(4726,-6586){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}Add $p(4,5)$ to $TB_t^2$}}}

3052: \put(4426,-6436){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{17}:$  $4<5$}}}

3053: \put(4351,-6886){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{18}:$   $\Box_t$}}}

3054: \put(3901,-3886){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$odd(Y),X$ is $Y+1,X<5$}}}

3055: \put(3976,-4336){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{13}:$  $Y$ is $2+1,Y<5,$}}}

3056: \put(3976,-4561){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$odd(Y),X$ is $Y+1,X<5$}}}

3057: \put(3676,-5011){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{14}:$ $3<5,odd(3),X$ is $3+1,X<5$}}}

3058: \put(3676,-5461){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{15}:$ $odd(3),X$ is $3+1,X<5$}}}

3059: \put(3901,-5986){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{16}:$  $X$ is $3+1,X<5$}}}

3060: \put(4726,-4786){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$Y=3$}}}

3061: \put(4726,-5236){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}Add $p(3,5)$ to $TB_t^2$}}}

3062: \put(7351,-3436){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{20}:$  $even(4),$}}}

3063: \put(7126,-3661){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$Y$ is $4+1,Y<5,$}}}

3064: \put(6976,-3886){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$odd(Y),X$ is $Y+1,X<5$}}}

3065: \put(7051,-4336){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{21}:$  $Y$ is $4+1,Y<5,$}}}

3066: \put(7051,-4561){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$odd(Y),X$ is $Y+1,X<5$}}}

3067: \put(7276,-5086){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{22}:$ $5<5,...$}}}

3068: \put(7651,-4936){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

3069: \put(3301,-3286){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

3070: \put(6226,-3286){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

3071: \put(9076,-3286){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$\Box_f$}}}

3072: \put(8776,-3436){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{23}:$  $even(1),...$}}}

3073: \put(3451,-3061){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$p(1,5)$}}}

3074: \put(4801,-3061){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$p(2,5)$}}}

3075: \put(6376,-3061){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$p(3,5)$}}}

3076: \put(7876,-3061){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$p(4,5)$}}}

3077: \put(9151,-3061){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$C_{p_3}$}}}

3078: \put(5926,614){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_0:$ $p(X,5)$ }}}

3079: \put(3151, 14){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_1:$   $\Box_t$}}}

3080: \put(3976, 14){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_2:$   $\Box_t$}}}

3081: \put(5026, 14){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_3:$  $loop(5),p(Y,5),odd(Y),X$ is $Y+1,X<5$}}}

3082: \put(5251,-436){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_4:$  $p(Y,5),odd(Y),X$ is $Y+1,X<5$}}}

3083: \put(6376,-211){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$C_{l_1}$}}}

3084: \put(9226,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}$p(4,5)$}}}

3085: \end{picture}

3086: 

3087: 

3088: \caption{$GT_{G_0}^2$. $\qquad\qquad\qquad\qquad\qquad$}\label{fig5-5}

3089: \end{figure}

3090: 

3091: Since $P_3$ is a positive program, $SLT(P_3,G_0,CS,\emptyset,\emptyset)

3092: =SLTP(P_3,G_0,CS,\emptyset,\emptyset)$. The first generalized SLT-tree

3093: $GT_{G_0}^1$ is shown in Figure \ref{fig5-4}. We

3094: explain a few main points. At $N_3$ the (non-looping) program

3095: clause $C_{p_3}$ is applied to $p(Y_1,5)$, which yields the

3096: first tabled answer $p(1,5)$. $p(1,5)$ is immediately added to 

3097: the table $TB_t^1$. After the failure of $N_4$, we 

3098: backtrack to $N_3$ and then $N_2$. By this time $C_{p_3}$

3099: has been completely used by $p(Y_1,5)$ at $N_3$, so we set 

3100: $comp\_used(p(Y_1,5),C_{p_3})=Yes$. Due to this $C_{p_3}$ is skipped at

3101: $N_2$. Applying the first tabled answer $p(1,5)$ to $p(Y,5)$ at $N_2$ 

3102: generates $N_5$. At $N_8$ the second tabled answer $p(2,5)$

3103: is produced, which yields the first answer to $G_0$. 

3104: $p(2,5)$ is then applied to $p(Y,5)$ at $N_2$, leading to $N_9$.

3105: When we backtrack to $N_0$ from $N_9$, $C_{p_2}$ 

3106: has been completely used by $p(Y,5)$ at $N_2$. So both 

3107: $C_{p_2}$ and $C_{p_3}$ are ignored at $N_0$. The

3108: tabled answer $p(1,5)$ is then applied to $p(X,5)$ at $N_0$, yielding the second answer

3109: $p(1,5)$ to $G_0$ at $N_{10}$. Note that the tabled answer 

3110: $p(2,5)$ was obtained from a correct answer substitution

3111: for $p(X,5)$ at $N_0$, so it was used by $p(X,5)$ while

3112: it was generated. As a result, $GT_{G_0}^1$ is completed

3113: with the table $TB_t^1=\{p(1,5),p(2,5)\}$.

3114: 

3115: We then do the first recursion of SLT-resolution by calling

3116: $SLTP(P_3\cup TB_t^1,G_0,CS,TB_t^1,\emptyset)$, which builds the

3117: second generalized SLT-tree $GT_{G_0}^2$ as shown in Figure \ref{fig5-5}.

3118: From $GT_{G_0}^2$ we get two new tabled answers $p(3,5)$ and $p(4,5)$.

3119: That is, $TB_t^2=\{p(1,5),p(2,5),p(3,5),p(4,5)\}$.

3120: 

3121: The second recursion of SLT-resolution is done by calling

3122: $SLTP(P_3\cup TB_t^2,G_0,CS,TB_t^2,\emptyset)$, which

3123: produces no new tabled answers. Therefore SLT-resolution stops here.

3124: 

3125: }

3126: \end{example}

3127: 

3128: \begin{remark}

3129: {\em

3130: Consider node $N_{10}$ in $GT_{G_0}^2$ (Figure \ref{fig5-5}).

3131: For each tabled answer $p(E,N)$ with $E$ an even number,

3132: apply it to $p(Y_1,N)$ will always produce two new tabled answers

3133: $p(E+1,N)$ and $p(E+2,N)$. Since these new answers will

3134: be fed back immediately to $N_{10}$ for $p(Y_1,N)$ to use, all the 

3135: remaining answers of $G_0$ will be produced at $N_{10}$.

3136: This means that for any $N$ evaluating $p(X,N)$ requires doing

3137: at most two recursions of SLT-resolution.

3138: }

3139: \end{remark}

3140: 

3141: It is easy to combine Optimizations \ref{opt1}, \ref{opt2} and \ref{opt3} 

3142: with Definition \ref{slt-tree}, which leads to an algorithm

3143: for generating {\em optimized} SLT-trees based on a fixed

3144: depth-first control strategy, as described in appendix \ref{apx1}.

3145: This algorithm is useful for the implementation of SLT-resolution.

3146: 

3147: \subsection{Computational Complexity of SLT-Resolution}

3148: 

3149: Theorem \ref{termin-normal} shows that

3150: SLT-resolution terminates in finite time

3151: for any programs with the bounded-term-size property.

3152: In the above subsections we present three effective optimizations 

3153: for reducing redundant computations. In this subsection we prove

3154: the computational complexity of (the optimized) SLT-resolution.

3155: 

3156: SLT-resolution evaluates queries by building some generalized

3157: SLT-trees. So the size of these generalized SLT-trees, i.e.

3158: the number of edges (except for the dotted edges) in the trees,

3159: represents the major part of its computational complexity. Since each edge

3160: in an SLT-tree is generated by applying either a program clause

3161: or a tabled answer, the size of a generalized SLT-tree is the number of 

3162: applications of program clauses and tabled answers during the resolution.

3163: 

3164: The following notation is borrowed from \cite{chen96}.

3165: 

3166: \begin{definition}

3167: {\em

3168: Let $P$ be a program. Then $|P|$ denotes the number of clauses in $P$,

3169: and $\Pi_P$ denotes the maximum number of literals in the body of

3170: a clause in $P$. Let $s$ be an arbitrary positive integer. Then $N(s)$

3171: denotes the number of atoms of predicates in $P$ that are not variants 

3172: of each other and whose arguments do not exceed $s$ in size.

3173: }

3174: \end{definition}

3175: 

3176: \begin{theorem}

3177: \label{th5-5}

3178: Let $P$ be a program with the bounded-term-size property,

3179: $G_0=\leftarrow A$ be a top goal (with $A$ an atom), and $CS$

3180: be a fixed depth-first

3181: control strategy. Then the size of each generalized 

3182: SLT-tree $GT_{G_0}^i$ is $O(|P|N(s)^{\Pi_P+2})$ for some $s>0$.

3183: \end{theorem}

3184: 

3185: \noindent {\bf Proof:}

3186: Let $n$ be the maximum size of arguments in $A$. Since $P$ has

3187: the bounded-term-size property, neither subgoal nor tabled answer has 

3188: arguments whose size exceeds $f(n)$ for some function $f$. 

3189: Let $s=f(n)$. Then the number of distinct subgoals (up to

3190: variable renaming) in $GT_{G_0}^i$ is bounded by $N(s)$.

3191: 

3192: Let $B=p(.)$ be a subgoal. By Theorem \ref{th5-4}, each clause

3193: $C_{p_j}$ will be applied to all variant subgoals of $B$

3194: in $GT_{G_0}^i$ at most $N(s)+1$ times. So the number of applications

3195: of all program clauses to all selected subgoals in $GT_{G_0}^i$ is bounded by 

3196: \begin{equation}

3197: N(s)*|P|*(N(s)+1)

3198: \qquad\qquad\qquad\qquad\qquad\qquad \label{num-cl}

3199: \end{equation}

3200: Moreover, when a program clause is applied, it 

3201: introduces at most $\Pi_P$ subgoals. Since the number of tabled

3202: answers to each subgoal is bounded by $N(s)$, the $\Pi_P$ subgoals

3203: access at most $N(s)^{\Pi_P}$ times to tabled answers. Hence the number of

3204: applications of tabled answers to all subgoals in $GT_{G_0}^i$ 

3205: is bounded by 

3206: \begin{equation}

3207: N(s)*|P|*(N(s)+1)*N(s)^{\Pi_P}

3208: \qquad\qquad\qquad\qquad\qquad \label{num-ans}

3209: \end{equation}

3210: Therefore the size of $GT_{G_0}^i$ is bounded by $(\ref{num-cl}) + (\ref{num-ans})$,

3211: i.e. $O(|P|N(s)^{\Pi_P+2})$. $\Box$

3212: 

3213: \vspace{4mm}

3214: 

3215: The second part of the computational complexity of SLT-resolution comes from

3216: loop checking, which occurs during the determination of looping

3217: clauses (see point 3 of Definition \ref{slt-tree}). Let $A_k=p(.)$ be 

3218: a selected subgoal at node $N_k$ in $GT_{G_0}^i$ and 

3219: $AL_{A_k}=\{(N_{k-1},A_{k-1}),...,(N_0,A_0)\}$ be its ancestor list.

3220: For convenience we express the ancestor-descendant relationship in

3221: $AL_{A_k}$ as a path like

3222: \begin{equation}

3223: N_0:A_0\Rightarrow_{C_{A_0}}...N_j:A_j\Rightarrow_{C_{A_j}}

3224: ...N_{k-1}:A_{k-1}\Rightarrow_{C_{A_{k-1}}} N_k: A_k

3225: \qquad\qquad\qquad \label{ans-des}

3226: \end{equation}

3227: where $C_{A_j}$ is a program clause used by $A_j$. By Definitions

3228: \ref{alist} and \ref{loop-def}, $N_0$ is the root of $GT_{G_0}^i$

3229: and $A_j$ is an ancestor subgoal of $A_{j+l}$ $(0\leq j<k, l>0)$.

3230: If $A_j$ is a variant of $A_k$, a loop occurs between $N_j$ and $N_k$

3231: so that the looping clause $C_{A_j}$ will be skipped by $A_k$.

3232: 

3233: It is easily seen that $k$ subgoal comparisons may be made to check

3234: if $A_k$ has ancestor variants. So if we do such loop checking for

3235: every $A_j$ in the path, then we may need $O(K^2)$ comparisons.

3236: 

3237: By Optimization \ref{opt3} program clauses are selected in a fixed

3238: order which is specified by a fixed control strategy. Let all clauses

3239: with head predicate $p$ be selected in the order: $C_{p_1},C_{p_2},

3240: ...,C_{p_m}$. Then $A_k$ and all its ancestor variant subgoals

3241: should follow this order. Assume $A_j$ is the closest ancestor

3242: variant subgoal of $A_k$ in the path (\ref{ans-des}). Let

3243: $C_{A_j}=C_{p_l}$. Then by Optimization \ref{opt3} each 

3244: $C_{p_h}$ $(h<l)$ either is a looping clause of $A_j$ or 

3245: has been completely used by a variant of $A_j$. This applies to $A_k$

3246: as well. So $A_k$ should skip all $C_{p_h}$s $(h\leq l)$. 

3247: This shows the following important fact.

3248: 

3249: \begin{fact}

3250: \label{f1}

3251: {\em

3252: To determine looping clauses or clauses that have been

3253: completely used for $A_k$, it suffices to find the closest

3254: ancestor variant subgoal of $A_k$.

3255: }

3256: \end{fact}

3257: 

3258: \begin{theorem}

3259: \label{th5-6}

3260: Let $P$ be a program with the bounded-term-size property,

3261: $G_0=\leftarrow A$ be a top goal (with $A$ an atom), and $CS$

3262: be a fixed depth-first 

3263: control strategy. Then the number of subgoal comparisons

3264: performed in searching for the closest ancestor variant subgoals 

3265: of all selected subgoals in  each generalized 

3266: SLT-tree $GT_{G_0}^i$ is $O(|P|N(s)^3)$.

3267: \end{theorem}

3268: 

3269: \noindent {\bf Proof:}

3270: Note that loop checking only relies on ancestor lists of subgoals, which

3271: only depend on program clauses with non-empty bodies (see Definition

3272: \ref{alist}). By formula (\ref{num-cl}) in the proof of Theorem \ref{th5-5},

3273: the total number of applications of program clauses to all selected

3274: subgoals in $GT_{G_0}^i$ is bounded by $N(s)*|P|*(N(s)+1)$. 

3275: Since each subgoal in the ancestor-descendant path (\ref{ans-des})

3276: has at most $|P|$ ancestor variant subgoals (i.e. the first variant uses the first

3277: program clause, the second uses the second, ..., and the $|P|$-th uses

3278: the last program clause), the length of the path

3279: is bounded by $N(s)*|P|$. Assume in the worst case that all $N(s)*|P|*(N(s)+1)$ 

3280: applications of clauses generate $N(s)+1$ ancestor-descendant paths

3281: like (\ref{ans-des}) of length $N(s)*|P|$. Since

3282: each subgoal in a path needs at most $N(s)$ comparisons to find its

3283: closest ancestor variant subgoal, the number of comparisons for

3284: all subgoals in each path is bounded by $N(s)*|P|*N(s)$. Therefore,

3285: the total number of subgoal comparisons in $N(s)+1$ paths

3286: is bounded by

3287: \begin{equation}

3288: N(s)*|P|*N(s)*(N(s)+1)

3289: \qquad\qquad\qquad\qquad\qquad\qquad \label{num-comp}

3290: \end{equation}  

3291: i.e. $O(|P|N(s)^3)$. $\Box$

3292: 

3293: \vspace{4mm}

3294: 

3295: Combining Theorems \ref{th5-5} and \ref{th5-6} and Fact \ref{f1} 

3296: leads to the following.

3297: 

3298: \begin{theorem}

3299: \label{th5-7}

3300: The time complexity of SLT-resolution is $O(|P|N(s)^{\Pi_P+3}log N(s))$.

3301: \end{theorem}

3302: 

3303: \noindent {\bf Proof:}

3304: The time complexity of SLT-resolution consists of the part of

3305: accessing program clauses, which is formula (\ref{num-cl}) times the complexity

3306: of accessing one clause, the part of accessing tabled answers,

3307: which is formula (\ref{num-ans}) times the complexity

3308: of accessing one tabled answer,

3309: and the part of subgoal comparisons in loop checking,

3310: which is formula (\ref{num-comp}) times the complexity

3311: of comparing two subgoals. The access

3312: to one program clause and the comparison of two subgoals

3313: can be assumed to be in constant time. A global table of subgoals 

3314: and their answers can be maintained, so that the time for retrieving and 

3315: inserting a tabled answer can be assumed to be $O(log N(s))$.

3316: So the time complexity of constructing one generalized SLT-tree $GT_{G_0}^i$ is

3317: \begin{equation}

3318: O((\ref{num-cl}) + (\ref{num-ans})*log N(s) + (\ref{num-comp}))

3319: =O(|P|N(s)^{\Pi_P+2}log N(s))

3320: \qquad\qquad\

3321: \end{equation}

3322: Since the number of $GT_{G_0}^i$s, i.e. the number of recursions of 

3323: SLT-resolution, is bounded by $N(s)$ (since each $GT_{G_0}^i$ produces

3324: at least one new tabled answer), the time complexity of SLT-resolution is

3325: $O(|P|N(s)^{\Pi_P+3}log N(s))$. $\Box$

3326: 

3327: \vspace{4mm}

3328: 

3329: It is shown in \cite{VRS91} that the {\em data complexity} of

3330: the well-founded semantics, as defined by Vardi \cite{vardi82},

3331: is polynomial time for function-free programs. 

3332: This is obviously true with SLT-resolution because in this case, $s=1$ and 

3333: $N(1)$ is a polynomial in the size of the {\em extensional

3334: database} (EDB) \cite{chen96}.

3335: 

3336: \section{Related Work}

3337: 

3338: So far only two operational 

3339: procedures for top-down evaluation of the well-founded

3340: semantics of general logic programs have been extensively

3341: studied: Global SLS-resolution and SLG-resolution. 

3342: Global SLS-resolution is not effective

3343: since it is not terminating even for function-free

3344: programs \cite{Prz89, Ross92}. Therefore, in this section  we make

3345: a detailed comparison of SLT-resolution with SLG-resolution.

3346: 

3347: There are three major differences between these two approaches. First,

3348: SLG-resolution is based on program

3349: transformations, instead of on standard tree-based formulations

3350: like SLDNF- or Global SLS-resolution. Starting from the predicates

3351: of the top goal, it transforms (instantiates) a set of clauses, called a

3352: {\em system}, into another system based on six basic transformation 

3353: rules. A special class of literals, called {\em delaying literals},

3354: is used to represent and handle

3355: temporarily undefined negative literals.

3356: Negative loops are identified by maintaining a {\em dependency graph}

3357: of subgoals \cite{CSW95, chen96}. In contrast, SLT-resolution is based on SLT-trees

3358: in which the flow of the query evaluation is naturally depicted by the ordered

3359: expansions of tree nodes.

3360: It appears that this style of formulations is easier for users to understand and 

3361: keep track of the computation. In addition, SLT-resolution handles temporarily 

3362: undefined negative literals simply by replacing them with $u^*$, and 

3363: treats positive and negative loops in the same way based on ancestor 

3364: lists of subgoals. 

3365: 

3366: The second difference is that like all existing tabling methods,

3367: SLG-resolution adopts the solution-lookup mode. Since all variant 

3368: subgoals acquire answers from the same source $-$ the solution node,

3369: SLG-resolution essentially generates a search graph instead of a

3370: search tree, where every lookup node has a hidden edge towards

3371: the solution node, which demands the solution node to produce 

3372: new answers. Consequently it has to jump back and forth between

3373: lookup and solution nodes. This is the reason why

3374: SLG-resolution is not linear for query evaluation. In contrast, SLT-resolution makes

3375: linear tabling derivations by generating SLT-trees. SLT-trees

3376: can be viewed as SLDNF-trees with no infinite loops and with

3377: significantly less redundant sub-branches.

3378: 

3379: Since SLG-resolution deviates from SLDNF-resolution,

3380: some standard Prolog techniques for the implementation of SLDNF-resolution, 

3381: such as the depth-first control strategy 

3382: and the efficient stack-based memory management,\footnote{Bol and 

3383: Degerstedt \cite{BD93} defined a special depth-first strategy that may be suitable

3384: for SLG-resolution. However, their definition of ``depth-first''

3385: is quite different from the standard one used in Prolog \cite{Ld87, NM95}.} 

3386: cannot be used for its

3387: implementation. This shows a third essential difference. SLT-resolution

3388: bridges the gap between the well-founded semantics

3389: and standard Prolog implementation techniques, and

3390: can be implemented by an extension to any existing Prolog abstract machines 

3391: such as WAM or ATOAM.  

3392: 

3393: The major shortcoming of SLT-resolution is that it is a little more time

3394: costly than SLG-resolution. The time complexity of SLG-resolution

3395: is $O(|P|N(s)^{\Pi_P+1}log N(s))$ \cite{chen96}, whereas ours is

3396: $O(|P|N(s)^{\Pi_P+3}log N(s))$ (see Theorem \ref{th5-7}). The extra

3397: price of our approach, i.e. $O(N(s))$ recursions (see Definition \ref{slt})

3398: and $O(N(s))$ applications of each program clause to each distinct 

3399: (up to variable renaming) subgoal (see Theorem \ref{th5-4}), 

3400: is paid for the preservation of the linearity

3401: for query evaluation. It should be pointed out, however, that

3402: in practical situations, the number of recursions and that of clause 

3403: applications are far less than $O(N(s))$. We note that in many typical cases,

3404: such as Examples \ref{eg3-3}, \ref{eg5-2} and \ref{dsz}, 

3405: both numbers are less than $3$. Moreover, the efficiency of SLT-resolution

3406: can be further improved by completing its recursions locally; see

3407: \cite{shen2000} for such special techniques.

3408: 

3409: Finally, for space consumption we note that SLG-resolution takes much more space

3410: than SLT-resolution. The solution-lookup mode used in SLG-resolution 

3411: requires that solution nodes stay forever

3412: whenever they are generated even if they will never be invoked later.

3413: In contrast, SLT-resolution will easily reclaim the space through backtracking

3414: using the efficient stack-based memory structure.

3415: 

3416: \section{Conclusion}

3417: We have presented a new operational procedure, SLT-resolution,

3418: for the well-founded semantics of general logic programs. Unlike

3419: Global SLS-resolution, it is free of infinite loops and with significantly 

3420: less redundant sub-derivations; it terminates for all programs

3421: with the bounded-term-size property. Unlike SLG-resolution, it preserves

3422: the linearity of SLDNF-resolution, which bridges the gap between

3423: the well-founded semantics and standard Prolog implementation techniques.

3424: 

3425: Prolog has many well-known nice features, but the problem

3426: of infinite loops and redundant computations considerably 

3427: undermines its beauties. The general goal of our research is then

3428: to extend Prolog with tabling 

3429: to compute the well-founded semantics while resolving infinite

3430: loops and redundant computations. SLT-resolution serves as a nice model for 

3431: such an extension. (Note that XSB \cite{SSW94, SSWFR98} 

3432: is the only existing system that top-down computes the well-founded semantics

3433: of general logic programs, but it is not an extension of Prolog since

3434: SLG-resolution and SLDNF-resolution are 

3435: totally heterogeneous.) 

3436: 

3437: For positive programs, we have developed special

3438: methods for the implementation of SLT-resolution based

3439: on the control strategy used by Prolog \cite{shen2000}.

3440: The handling of cuts of Prolog is also discussed there.

3441: A preliminary report on methods for the implementation of

3442: SLT-resolution for general logic programs appears in \cite{shen99}.

3443: 

3444: \section*{Acknowledgements}

3445: The first author is supported in part by Chinese National

3446: Natural Science Foundation and Trans-Century Training Program

3447: Foundation for the Talents by the Chinese Ministry of Education.

3448: 

3449: \appendix

3450: \section{Optimized SLT-Trees}

3451: \label{apx1}

3452: 

3453: Assume that program clauses and tabled answers are

3454: stored separately, and that new tabled positive answers in SLT-trees 

3455: are added into the table $TB_t$ once they are generated (see Section \ref{sec-dup}).

3456: Combining Optimizations \ref{opt1}, \ref{opt2} and \ref{opt3} in Section \ref{sec5} 

3457: with Definition \ref{slt-tree}, we obtain an algorithm

3458: for generating optimized SLT-trees based on a fixed

3459: depth-first control strategy. 

3460: 

3461: \begin{definition}[SLT-trees, an optimized version]

3462: \label{opslt-tree}

3463: {\em

3464: Let $P=P^c\cup TB_t$ be a program with $P^c$ a set of program clauses

3465: and $TB_t$ a set of tabled positive answers. Let $G_0$ be a top goal 

3466: and $CS$ be a depth-first control strategy.

3467: Let $TB_f$ be a set of ground atoms such that for each $A\in TB_f$ $\neg A\in WF(P)$.

3468: The {\em optimized SLT-tree} $T_{G_0}$ for $(P \cup \{G_0\},TB_f)$ via $CS$ is a tree

3469: rooted at node $N_0:G_0$, which is generated as follows.

3470: 

3471: \begin{enumerate}

3472: \item

3473: Select the root node for expansion.

3474: 

3475: \item

3476: \label{l1} (Node Expansion)

3477: Let $N_i:G_i$ be the node selected for expansion, with $G_i=\leftarrow L_1,...,L_n$. 

3478: 

3479: \begin{enumerate}

3480: \item

3481: If $n=0$ then mark $N_i$ by $\Box_t$ (a {\em success} leaf) and

3482: goto \ref{l2} with $N=N_i$.

3483: 

3484: \item

3485: If $L_1=u^*$ then mark $N_i$ by $\Box_{u^*}$ (a {\em temporarily undefined} 

3486: leaf) and goto \ref{l2} with $N=N_i$.

3487: 

3488: \item

3489: \label{l13}

3490: Let $L_j$ be a positive literal selected by $CS$. Select a tabled answer

3491: or program clause, $C$, from $P$ based on $CS$ 

3492: while applying Optimizations \ref{opt2}

3493: and \ref{opt3}. If $C$ is empty, then if $N_i$ has already had child nodes then

3494: goto \ref{l2} with $N=N_i$ else mark $N_i$ by $\Box_f$ (a {\em failure} leaf)

3495: and goto \ref{l2} with $N=N_i$. Otherwise, $N_i$ has a new child node labeled by

3496: the resolvent of $G_i$ and $C$ over the literal $L_j$. Select the new child node

3497: for expansion and goto \ref{l1}.

3498: 

3499: \item

3500: Let $L_j=\neg A$ be a negative ground literal selected by $CS$. If  

3501: $A$ is in $TB_f$ then $N_i$ has only one child that is labeled

3502: by the goal $\leftarrow L_1,...,L_{j-1},L_{j+1},...,L_n$,

3503: select this child node for expansion, and goto \ref{l1}. 

3504: Otherwise, build an optimized SLT-tree

3505: $T_{\leftarrow A}$ for $(P \cup \{\leftarrow A\},TB_f)$ via $CS$, where 

3506: the subgoal $A$ at the root inherits the ancestor

3507: list $AL_{L_j}$ of $L_j$. We consider the following cases:

3508: 

3509: \begin{enumerate}

3510: \item

3511: If $T_{\leftarrow A}$ has a success leaf then mark

3512: $N_i$ by $\Box_f$ and goto \ref{l2} with $N=N_i$;

3513: 

3514: \item

3515: \label{l142}

3516: If the root of $T_{\leftarrow A}$ is loop-independent

3517: and all branches of $T_{\leftarrow A}$ end with a failure leaf

3518: then $N_i$ has only one child that is labeled

3519: by the goal $\leftarrow L_1,...,L_{j-1},L_{j+1},...,L_n$,

3520: select this child node for expansion, and goto \ref{l1};

3521: 

3522: \item

3523: Otherwise, $N_i$ has only one child that is labeled

3524: by the goal $\leftarrow L_1,...,L_{j-1},L_{j+1},$ $..., L_n,u^*$ if $L_n\neq u^*$

3525: or $\leftarrow L_1,...,L_{j-1},L_{j+1},...,L_n$ if $L_n= u^*$. 

3526: Select this child node for expansion and goto \ref{l1}.

3527: \end{enumerate}

3528: \end{enumerate}

3529: \item

3530: \label{l2} (Backtracking)

3531: If $N$ is loop-independent and the selected literal $A$ at $N$

3532: is positive then set $comp(A)=Yes$. If $N$ is the root node then return.

3533: Otherwise, let $N_f:G_f$ be the parent node of $N$, with the selected

3534: literal $L_f$. If $L_f$ is negative then goto \ref{l2} with $N=N_f$.

3535: Else, if $N$ was generated from $N_f$ by resolving $G_f$ with a program

3536: clause $C$ on $L_f$ then set $comp\_used(L_f,C)=Yes$.

3537: Select $N_f$ for expansion and goto \ref{l1}.

3538: \end{enumerate} 

3539: }

3540: \end{definition}

3541: 

3542: Optimization \ref{opt1} is used at item \ref{l142}.

3543: Optimizations \ref{opt2} and \ref{opt3} are applied at item \ref{l13}

3544: for the selection of program clauses. The flags $comp(\_)$ and 

3545: $comp\_used(\_,\_)$ are updated during backtracking (point \ref{l2}).

3546: The flag $loop\_depend(\_)$ is assumed to be updated automatically based

3547: on loop dependency of nodes.

3548: 

3549: \begin{thebibliography}{59} 

3550: \bibitem{AV82} K. R. Apt, M. H. Van Emden,

3551: Contributions to the theory of logic programming,

3552: {\it J. ACM} 29(3):841-862 (1982).

3553: 

3554: \bibitem{BAK91} R. N. Bol, K. R. Apt and J. W. Klop,

3555: An analysis of loop checking mechanisms for logic

3556: programs, {\em Theoretical Computer Science} 86(1):35-79 (1991).

3557: 

3558: \bibitem{BD93} R. N. Bol and L. Degerstedt,

3559: The underlying search for magic templates and

3560: tabulation, in: {\em Proc. of the Tenth 

3561: International Conference on Logic Programming},

3562: MIT Press, 1993.

3563: 

3564: \bibitem{BD98} R. N. Bol and 

3565: L. Degerstedt, Tabulated resolution for the well-founded semantics.

3566: {\em Journal of Logic Programming} 34(2):67-109 (1998).

3567: 

3568: \bibitem{chan88} D. Chan, Constructive negation based on the 

3569: completed database, in: (R. A. Kowalski and K. A. Bowen, eds.)

3570: {\em Proc. of the Fifth International Conference and Symposium

3571: on Logic Programming}, Seattle, USA, MIT Press, 1988, pp. 111-125.

3572: 

3573: \bibitem{CSW95} W. D. Chen, T. Swift and D. S. Warren,

3574: Efficient top-down computation of queries under the

3575: well-founded semantics, {\em Journal of Logic Programming}

3576: 24(3):161-199 (1995).

3577: 

3578: \bibitem{chen96} W. D. Chen and D. S. Warren, Tabled evaluation with

3579: delaying for general logic programs, {\it J. ACM} 43(1):20-74 (1996).

3580: 

3581: \bibitem{clark78} K. L. Clark, Negation as Failure, in:

3582: (H. Gallaire and J. Minker, eds.) {\em Logic and Databases},

3583: Plenum, New York, 1978, pp. 293-322.

3584: 

3585: \bibitem{DD93} D. De Schreye and S. Decorte, Termination of

3586: logic programs: the never-ending story, {\em Journal of Logic 

3587: Programming} 19/20:199-260 (1993).

3588: 

3589: \bibitem{dra95} W. Drabent, What is failure? An approach to constructive

3590: negation, {\em Acta Informatica} 32(1):27-59 (1995).

3591: 

3592: \bibitem{GL88} M. Gelfond and V. Lifschitz, The stable model semantics

3593: for logic programming, in: (R. A. Kowalski and K. A. Bowen, eds.)

3594: {\em Proc. of the Fifth International Conference and Symposium

3595: on Logic Programming}, Seattle, USA, MIT Press, 1988, pp. 1070-1080.

3596: 

3597: \bibitem{KK71} R. A. Kowalski and D. Kuehner, Linear resolution

3598: with selection functions, {\em Artificial Intelligence}

3599: 2:227-260 (1971).

3600: 

3601: \bibitem{Kow74} R. A. Kowalski, Predicate logic as a programming

3602: language, {\em IFIP} 74, pp.569-574.

3603: 

3604: \bibitem{LAC99} J. Y. Liu, L., Adams, and W. Chen, Constructive negation 

3605: under the well-founded semantics, {\em Journal of Logic 

3606: Programming} 38(3):295-330 (1999).

3607: 

3608: \bibitem{Ld87} J. W. Lloyd, {\em Foundations of Logic Programming},

3609: 2nd ed., Springer-Verlag, Berlin, 1987.

3610: 

3611: \bibitem{NM95} U. Nilsson and J. Maluszynski, {\em Logic Programming

3612: and Prolog}, 2nd ed., John Wiley \& Sons, 1995.

3613: 

3614: \bibitem{Prz89-2} T. Przymusunski, On the declarative and procedural

3615: semantics of logic programs, {\em Journal of Automated Reasoning}

3616: 5:167-205 (1989).

3617:  

3618: \bibitem{Prz89} T. Przymusunski, Every logic program has a natural 

3619: stratification and an iterated fixed point model, in: {\em Proc. of the   

3620: 8th ACM Symposium on Principles of Database Systems}, 1989, pp. 11-21.

3621: 

3622: \bibitem{Prz89-3} T. Przymusunski, On constructive negation 

3623: in logic programming, in: (E. L. Lusk and R. A. Overbeek eds.)

3624: {\em Proc. of the North American Conference on Logic Programming},

3625: Ohi, USA, MIT Press, 1989, page (Addendum to the Volume).

3626: 

3627: \bibitem{Prz90} T. Przymusunski, The well-founded semantics coincides 

3628: with the three-valued stable semantics, {\em Fundamenta Informaticae}

3629: 13:445-463 (1990).

3630: 

3631: \bibitem{Robinson65} J. A. Robinson, A machine-oriented logic

3632: based on the resolution principle, {\it J. ACM} 12(1):23-41 (1965).

3633:  

3634: \bibitem{Ross92} K. Ross, A procedural semantics for well-founded 

3635: negation in logic programs, {\em Journal of Logic Programming}  

3636: 13(1):1-22 (1992).  

3637: 

3638: \bibitem{SSW94} K. Sagonas, T. Swift and D. S. Warren,

3639: XSB as an efficient deductive database engine,

3640: in: {\em Proc. of the ACM SIGMOD Conference on Management of Data},

3641: Minneapolis, 1994, pp. 442-453.

3642: 

3643: \bibitem{SSW98} K. Sagonas and T. Swift,

3644: An abstract machine for tabled execution of fixed-order

3645: stratified logic programs, {\it ACM Transactions on

3646: Programming Languages and Systems}, 20(3) (1998).

3647: 

3648: \bibitem{SSWFR98}  K. Sagonas, T. Swift, D. S. Warren, J. Freire

3649: and P. Rao, {\em The XSB Programmer's Manual (Version 1.8)},

3650: 1998.

3651: 

3652: \bibitem{shen97} Y. D. Shen, An extended variant of

3653: atoms loop check for positive logic programs, 

3654: {\em New Generation Computing} 15(2):187-204 (1997).

3655: 

3656: \bibitem{shen2000} Y. D. Shen, L. Y. Yuan, J. H. You, and N. F. Zhou,

3657: Linear tabulated resolution based on Prolog control strategy, 

3658: {\em Theory and Practice of Logic Programming} 

3659: (previously {\em Journal of Logic Programming}), to appear. 

3660: 

3661: \bibitem{shen99} Y. D. Shen, L. Y. Yuan, J. H. You and N. F. Zhou,

3662: Linear tabulated resolution for the well founded semantics,

3663: in: {\it Proc. of the 5th International Conference on 

3664: Logic Programming and Nonmonotonic Reasoning,} 

3665: Texas USA, 1999, pp. 192-205. 

3666: 

3667: \bibitem{sheph88} J. C. Shepherdson, Negation in logic programming,

3668: in: (J. Minker, ed.) {\em Foundations of Deductive Databases

3669: and Logic Programming}, Morgan Kaufmann, 1988, pp. 19-88.

3670: 

3671: \bibitem{TS86} H. Tamaki and T. Sato, OLD resolution with tabulation,

3672: in: {\it Proc. of the Third International Conference on Logic

3673: Programming}, London, 1986, pp. 84-98.

3674: 

3675: \bibitem{EK76} M. H. Van Emden and R. A. Kowalski, The 

3676: semantics of predicate logic as a programming

3677: language, {\it J. ACM} 23(4):733-742 (1976).

3678: 

3679: \bibitem{VG89} A. Van Gelder, Negation as failure using tight 

3680: derivations for general logic programs, 

3681: {\em Journal of Logic Programming} 6(1\&2):109-133 (1989).

3682:  

3683: \bibitem{VRS91} A. Van Gelder, K. Ross, J. Schlipf, The  

3684: well-founded semantics for general logic programs, 

3685: {\em J. ACM} 38(3):620-650 (1991).

3686: 

3687: \bibitem{vardi82} M. Vardi, The complexity of relational query

3688: languages, in: {\em ACM Symposium on Theory of Computing}, 

3689: 1982, pp. 137-146.

3690: 

3691: \bibitem{VL89} L. Vieille, Recursive query processing:

3692: the power of logic, {\em Theoretical Computer Science} 69:1-53 (1989).

3693: 

3694: \bibitem{WAM83} D. H. D. Warren, An abstract Prolog instruction

3695: set, Technical Report 309, SRI International, 1983.

3696: 

3697: \bibitem{war92} D. S. Warren, Memoing for logic programs, 

3698: {\em CACM} 35(3):93-111 (1992).

3699: 

3700: \bibitem{ZHOU96} N. F. Zhou, Parameter passing and  control stack

3701: management in Prolog implementation revisited, 

3702: {\it ACM Transactions on

3703: Programming Languages and Systems}, 18(6):752-779 (1996).

3704: 

3705: \end{thebibliography} 

3706:  

3707: \end{document} 

3708:  

3709:   

3710: