
## 5.1 Annotated And Acyclic Derivations

An annotated literal (*a-literal* for short) is a pair Lα where L is a literal and α is an annotation, that is, a sequence of atoms. The empty annotation will be denoted with ε. Lα is *positive* (resp. *negative*) if L is positive (resp. negative). An annotated goal *(a-goal* for short) is a finite sequence G = L1α1**, . . . , L**nαn of annotated literals. An annotated goal is *cyclic* if some positive Li occurs in αi, *acyclic* otherwise.

Given an a-goal G = L1α1**, . . . , L**nαn, a positive Liαiin G (1 ≤ i ≤ n), and a rule R = A ← L
′

1
, . . . , L′m such that Li and A are unifiable and mgu(Li, A) = θ, the goal L1α1, . . . , Li−1αi−1, L′1α
′
**, . . . , L**′mα
′
, Li+1αi+1**, . . . , L**nαnθ where α
′ = Li·αiis called the *annotated resolvent* of G, Li, and R with mgu θ. The atom Liis called *selected atom*, and in this paper it will always be the *leftmost positive literal* of G. Accordingly, the selected literal will frequently be omitted.

An annotated derivation (*a-derivation* for short) of G0 from a program P with rules R1, . . . , Ri**, . . .** and mgu's θ1, . . . , θi**, . . .** is a (possibly infinite) sequence of a-goals G0, . . . , Gi**, . . .** such that each Gj in the sequence with j > 0 is the annotated resolvent of Gj−1 and Rj with mgu θj , for some standardized apart variant Rj of a rule in P. An a-derivation is *acyclic* if all of its a-goals are, possibly with the exception of the last goal if the derivation is finite. Intuitively, an acyclic derivation *fails* as soon as a cycle is detected.

An a-derivation is *successful* if it is finite and its last element contains no positive aliterals. If G0**, . . . , G**n is a successful a-derivation with mgu's θ1**, . . . , θ**n, then we call the composition θ g = θ1 **◦ · · · ◦** θn a *global answer* to G0, and the restriction of θ gto the variables of G0 an *answer substitution* to G0.

## Example 5.1

Consider the program P consisting of the rules p(X) ← q(X), q(X) ← p(X), and p(a).

The goal p(a) has both a successful acyclic a-derivation p(a)ε, ✷ (where ✷ denotes the empty goal) where p(a) is resolved with the third rule, and a failed acyclic derivation using the first two rules: p(a)ε, q(a)p(a), p(a)(q(a) · p(a)). The underlined literals show that the last goal is cyclic.

The main results of the paper will need the following technical definitions and lemmata.

Let G0 be an a-goal with at least k positive a-literals. An *embedded a-derivation of* degree k for G0 is an a-derivation ∆ = G0, G1**, . . .** such that for some suffix G′′ of G0:

- for all i = 0, 1**, . . .**, it holds Gi = G′iG′′, for some G′i
;
- the number of positive a-literals in G′0 is k;
- if ∆ is finite and Gn is its last goal, either G′n has no positive a-literals or G′n is failed; in the former case, the embedded a-derivation is *successful*, otherwise it is failed.
Intuitively, an embedded derivation of degree k, if successful, resolves the first k positive literals of the initial goal. In the following sections, we will sometimes split derivations into multiple embedded derivations to apply the induction hypotheses. The following two lemmata help.