1 Definitions and Notation

We list some relevant notions^{1}.

Definition 1.1 [Terms as trees] Consider ⟨N^{∗}, ·, ∗⟩, the monoid of sequences of natural numbers, called positions with concatenation as the binary operator and the empty sequence as the neuter element. Further, we call a set of positions P ⊆ N^{∗} prefix-closed iff for all p, q, r ∈ N^{∗}: p = q · r ⇒ q ∈ P. For p ∈ P, succ(p) = {q ∈ P | ∃i : q = p · i}. A term t over an signature Σ and an set X of variables is a pair ⟨t, l_{Σ}⟩ satisfying the following conditions:

1. P ⊆ N^{∗} is prefix-closed

2. l_{Σ} : P ⟶ Σ ∪ X

3. If root(t) = f and arity(f) = n > 0, then l_{Σ}(p) = f implies that the successors of p in P (t) are p · 1, …, p · n.

Definition 1.2 [Contexts] E[F] denotes that the subexpression F inside the brackets has at least one occurrence in E.

Definition 1.3 [Linear] A term u is linear if there is no multiple occurrence of the same variable therein. The term θt is called restricted w.r.t. t if either there is x ∈ t such that θx is not linear or there are two distinct variables x_{1}, x_{2} ∈ t such that θx_{1} and θx_{1} share a variable.

Definition 1.4 [Universal(Existential) closure]

Definition 1.5 [Substitutions]

Definition 1.6 [Ground, Instance, Term Subsumption]

Notation 1.1 (Tuples and variables) We write t⃗ for a tuple of elements, in this case terms, whose length is unimportant: \overline{t_{n}} will be used as an abbreviation of t_{1}, …, t_{n}. Note that this notation assumes the properies of finite sets, i.e. x⃗ stands both for x, x′ and x′, x. Further, \overline{x_{n}}, \overline{y_{m}}, \overline{z_{p}} and their vectorized version are intended to stand resp. for tuples (sets) of existential, universal and free variables. They are assumed to be disjoint: \overline{w_{r}} will be used to stand for a tuple of either free or existentially quantified variables. \overline{t_{m}} = \overline{s_{m}} (resp. \overline{t_{m}} ≠ \overline{s_{m}}) will stand for

⋀_{i=1}^{m} t_{i} = s_{i}  ⋁_{i=1}^{m} t_{i} ≠ s_{i}

taking the place sometimes of the more cumbersome notation

\overline{\overline{t_{m}} = \overline{\overline{s_{m}}}}

. Notation for substitution: [M/x]N.

1under construction

For a syntactic object O, F V (O) will denote the set of its free variables. Discussion of the \underline{U}niversal Query Problem: In Logic textbook a first-order

language usually contains an infinite set of function symbol. On the other hand, the signature of (the language of) a program is finite. in the logic programming community this seemingly innocent issue became hot w.r.t. the semantics of negation-as-failure. Kunen [?] and later Shepherdson [] advocated a return to the former approach which makes the treatment of CET nicer. Afterwards Maher [?] set the records straight (to be continued)