Theory of Generalized Annotated Logic Programming and its Applications^{∗}

Michael Kifer^{†} Department of Computer Science SUNY at Stony Brook Stony Brook, NY 11794. E-Mail: kifer@cs.sunysb.edu

V.S. Subrahmanian Department of Computer Science University of Maryland College Park, Maryland 20742. E-Mail: vs@cs.umd.edu

Abstract

Annotated logics were introduced in [43] and later studied in [5, 7, 31, 32]. In [31], annotations were extended to allow variables and functions, and it was argued that such logics can be used to provide a formal semantics for rule-based expert systems with uncertainty. In this paper we continue to investigate the power of this approach. First, we introduce a new semantics for such programs based on ideals of lattices. Subsequently, some proposals for multivalued logic programming [5, 7, 32, 47, 40, 18] as well as some formalisms for temporal reasoning [1, 3, 42] are shown to fit into this framework. As an interesting by-product of this investigation, we obtain a new result concerning multivalued logic programming: a model theory for Fitting’s bilattice-based logic programming, which until now has not been characterized model-theoretically. This is accompanied by a corresponding proof theory.

1 Introduction

Large knowledge bases can be inconsistent in many ways. Nevertheless, certain “localizable” inconsistencies should not be allowed to significantly alter the intended meaning of such knowledge bases. As classical logic semantics decrees that inconsistent theories have no models (and hence are meaningless from a model-theoretic point of view), classical logic is not the appropriate formalism for reasoning about inconsistent knowledge bases.

As a step towards the solution of this problem, annotated logic programs were introduced by Subrahmanian in [43] and were subsequently studied in [5, 7] by Blair and Subrahmanian. In [32, 33], Kifer and Lozinskii extended the theory to a full-fledged logic, and it was shown that a sound and complete proof procedure exists. More efficient proof procedures have been recently obtained, and implementations of these theorem provers have been designed (cf. [12, 26]). Kifer and Li [31] extended annotated programs in a different direction by allowing variables and evaluable function terms to appear as annotations. We will call such programs generalized annotated programs (GAPs, for short). The utility of annotated logics for reasoning with inconsistency and for programming expert systems was well argued in [5, 7, 31, 32, 33]. In this paper we continue to investigate the power of this formalism.

∗A preliminary report on this research has appeared in [34]

†Work supported in part by the NSF grant IRI-8903507.

First we extend the semantics of [7, 31, 32, 33] to allow annotation variables over arbitrary semilattices of truth values (in [31] only a special lattice - the Cartesian product of two unit intervals - was considered and in [7, 32, 33], the notion of annotation variable was not present). Then we present the model-theoretic, fixed-point, and operational semantics of GAPs. In Section 5.1 we show that van Emden’s quantitative logic programming [47] is a special case of GAPs. Then, in Section 5.2, we show how Fitting’s bilattice-based logic programming approach fits into the framework of GAPs. The consequence of this “fit” is that we can now characterize Fitting’s approach model-theoretically (no model-theoretic semantics was previously proposed for this approach). By translating [47] and [18] into GAPs, we obtain a sound and complete proof procedure for these theories, thus strengthening van Emden’s soundness and completeness theorems (which were obtained under some restrictions) and complementing Fitting’s results. Lastly, we demonstrate how to incorporate two versions of temporal logic programming in the framework of GAPs – in the first, we consider a discrete linear version of time, i.e., each instant of time is a time point; in the second, we consider an interval-based temporal logic. We show that GAPs are sufficiently expressive to be able to cope with a large body of temporal problems and, in particular, subsume some of the earlier proposals for temporal logic programming [3]. Although our approach cannot directly represent certain constructs used in temporal specifications, we note that the implication problem in most full-fledged temporal logics is Π_{1}^{1}-complete and therefore such logics cannot be adequately implemented on a computer, anyway. In contrast, the corresponding problem for temporal specifications in GAPs is semi-decidable and thus they are more suitable for a computer implementation.

We believe that this paper unifies, and in some cases, generalizes various results and treatments of multivalued logic programming. Furthermore, it presents new applications of this formal setting. So far, research in multivalued logic programming has proceeded along three different directions:

1. Annotated logics as described in [5, 7, 32, 33];

2. Bilattice-based logics [23, 17]; and

3. Quantitative rule sets [47, 39, 29, 36, 41, 28, 40].

Earlier studies of these three approaches quickly identified various distinctions between these frameworks. For example, one of the key insights behind bilattices was the interplay between the truth values assigned to sentences and the notion of implication in the language under consideration. Thus, rules (implications) had weights (or truth values) associated with them as a whole. The problem was to study how truth values should be propagated “across” implications. Annotated logics, on the other hand, appeared to associate truth values with each component of an implication rather than the implication as a whole. The implication itself was then interpreted in a “classical logic” fashion. The two approaches had their own advantages and disadvantages: although associating truth values with implications, as in [23], has intuitive appeal, annotated logics provide a simpler formalism that is much closer to classical logic. Besides, in [33] it is shown that for many problems in nonmonotonic reasoning, it is easier to arrive at the intended semantics via nonmonotonic annotated logics, compared to the bilattice-based formalism of [23].

However, one of the principal results of this paper is to show that this dichotomy can be done away with. The GAP framework introduced here uses the “classical” definition of implication in the same way as in [43, 7, 32]. However, by appropriately generalizing the concept of an annotation, we are able to capture the propagation of truth values “across” implications (cf. Theorems 7 and 8), at least to the extent this propagation is treated in [17]. This is one of the key insights provided by this paper.

Additionally, this paper demonstrates that the GAP framework can be used to implement a semi-decidable fragment of temporal logics, which is a new application for GAPs. Ginsberg [24] has recently observed that there are various connections between bilattices and modal logics, temporal logics in particular. However, his treatment of temporal logics is very sketchy and no semidecidable proof theory for a large enough fragment of such logics is given.

2 Generalized Annotated Logic Programs

We assume an upper semilattice T of truth values, and denote the semilattice ordering on T by ≤ and the least upper bound operator by ⊔. The semilattice needs not be complete. It is often convenient to assume the existence of a greatest element in T , denoted ⊤, and some of our results will depend on this assumption. The greatest lower bound operator, when it exists, is denoted by ⊓. Elements of T can be thought of as confidence factors [7, 31], or degrees of belief [7, 32, 33], or, as we shall see later, as truth values similar to those used in multivalued logics. In addition, sometimes it will be assumed that T has a unique least element, denoted ⊥; in these cases this assumption will be made explicitly.

For each i ≥ 1, we postulate that there is a family F_{i} of total continuous (hence monotonic) functions, each of type T^{i} → T , called annotation functions. We denote F = ∪_{i≥1}F_{i} and assume that all functions f in F are computable in the sense that there is a uniform procedure P_{f} such that if f is n-ary and μ_{1},…, μ_{n} are given as input to P_{f}, then f(μ_{1},…, μ_{n}) is output by P_{f} in a finite amount of time. We also assume that each F_{j} contains a j-ary function ⊔_{j}, derived from the semilattice operator ⊔, which, given inputs μ_{1},…, μ_{j}, returns the least upper bound of {μ_{1},…, μ_{j}}. Slightly abusing the notation, we will often write ⊔ instead of ⊔_{j}. Apart from the interpreted annotation functions, the language contains usual uninterpreted functions, constants, and predicate symbols, as commonly used in logic programs. We also postulate two disjoint sets of variable symbols – object variables, and annotation variables.

Definition 1 An annotation is either an element of T , an annotation variable, or a complex annotation term. Annotation terms are defined recursively as follows: members of T and variable annotations are annotation terms. In addition, if f ∈ F_{n} and x_{1},…, x_{n} are annotation terms, then f(x_{1},…, x_{n}) is a complex annotation term. If A is a usual atomic formula of predicate calculus (built out of object variables and uninterpreted predicate, function, and constant symbols) and α is an annotation, then A : α is an annotated atom. An annotated atom containing no occurrences of object variables is ground. If α ∈ T then A : α is constant-annotated (or c-annotated, for brevity). When α is an annotation variable, then A : α is said to be variable-annotated (v-annotated). If α is a complex annotation term then A : α is term-annotated (t-annotated).

Definition 2 If A : ρ is an annotated atom and B_{1} : μ_{1},…, B_{k} : μ_{k} are c- or v-annotated atoms, then

A : ρ ← B_{1} : μ_{1} & … & B_{k} : μ_{k}

is an annotated clause. A : ρ is called the head of this clause, while B_{1} : μ_{1} & … & B_{k} : μ_{k} is called the body. All variables (object or annotation) are implicitly universally quantified.

Any set of annotated clauses is also a generalized annotated program (abbr., a GAP).

Intuitively, what this definition says is that members of F may occur in the annotation of the head of a clause, but that elements of F may not occur in the body of a clause. For instance, if we take T to be the interval [0, 1] of real numbers, then

p(s(X)) : 0.5 × μ ← p(X) : μ

is a clause that says: If the truth value assigned to p(X) is μ, then p(s(X)) is assigned 0.5 × μ. In general, using this intuition, a quantitative rule

r : A ← B_{1} & … & B_{k}

of van Emden [47] may be translated into the annotated clause:

A : r × min{μ_{1},…, μ_{k}} ← B_{1} : μ_{1} & … & B_{k} : μ_{k}.

This issue will be further discussed in Section 5.1. We also note that

p(X) : μ ← p(s(X)) : 0.5 × μ

is not an annotated clause because it contains a complex annotation term in the clause-body.

Definition 3 Suppose C is an annotated clause. A c-annotated instance of C is any annotated clause obtained by replacing all annotation variables occurring in C by members of T . Different occurrences of the same annotation variable must be replaced by the same member of T .

Definition 4 Suppose C is an annotated clause. A strictly ground instance of C is any ground instance of C which contains only c-annotations. Notice that since all functions in F are evaluable, annotation terms of the form f(a_{1}, ..., a_{n}), where a_{1}, ..., a_{n} ∈ T and f ∈ F_{n}, are also considered to be ground and are identified with the result of the computation of f on the a_{i}’s.

We use the notation SGI(C) to denote the set of all strictly ground instances of a clause C. Similarly, if P is a GAP, then we denote the set of all strictly ground instances of clauses in P by SGI(P).

3 The General and Restricted Semantics

In this section, we propose two alternative model-theoretic semantics for GAPs. The first corresponds closely to that in [31, 34], while the second is ideal-theoretic in nature, first proposed in [33].

Definition 5 An ideal of an upper semilattice is any subset S such that:

• S is downward closed, i.e. s ∈ S and t ≤ s imply t ∈ S; and

• S is closed with respect to finite least upper bounds, i.e. s, t ∈ S implies s ⊔ t ∈ S.

An ideal S is principal if for some p ∈ T , S = {s|s ≤ p}. S is called the principal ideal generated by p and is denoted by ∥p∥. The set of all ideals of T is denoted by I(T ), and the set of principal ideals of T will be denoted by PI(T ). □

Example 1 Ideals are not necessarily closed under infinite least upper bounds. For example, consider the complete lattice [0, 1] (the unit interval of reals) ordered by the familiar “≤” relation. Then the right-open interval

[0, 1) = {x | 0 ≤ x < 1}

is an ideal which is not closed under the infinite least upper bound operator. □

It is easily seen that I(T ) forms a complete lattice with the intersection operation serving as the greatest lower bound and the union operator serving as the least upper bound; the order on I(T ) is determined by the usual set inclusion ⊆. Furthermore, there is a homomorphic embedding of upper semilattices T ⟼ I(T ) (that preserves finite least upper bounds) that maps elements of T into the corresponding principal ideals of I(T ).

Definition 6 Let L be a language of annotated logic. The Herbrand Base of L, B_{L}, is the set of all ground atomic formulas of L (without annotations). A general Herbrand interpretation (or just interpretation, for short) I is a mapping from the Herbrand Base of L to I(T ). Since I is a function into a partially ordered set I(T ), we can define a partial order on interpretations in the usual way: I ≤ J if and only if for every p ∈ B_{L}, I(p) ⊆ J(p).

A restricted Herbrand interpretation (r-interpretation, for short) of L is any map from B_{L} to T . Equivalently, a r-interpretation of L is a map from B_{L} to PI(T ), the set of principal ideals of T (this explains the name “restricted” for such interpretations). □

Note here the distinction between the two notions of interpretations. Restricted Herbrand interpretations assign a single truth value, i.e., essentially a principal ideal to ground atoms; in contrast, general interpretations assign arbitrary ideals to atoms. Therefore, every r-interpretation is also a general interpretation, but not vice versa. In the sequel, we will be freely switching between the two views of r-interpretations, i.e. we will think of them either as mappings B_{L} ↦ T or B_{L} ↦ PI(T ), depending on which of the views is more convenient at the moment. Following [32, 33], we could also define interpretations with arbitrary domains, but since in this paper we are mainly concerned with logic programming, we will restrict our attention to Herbrand interpretations only.

We assume that there is a unary operator ¬ : T → T , conceptually interpreted as negation. For the technical purposes of this paper, we do not need to impose any restrictions on ¬. However, sometimes one may wish ¬ to satisfy certain epistemological criteria, such as ¬ being a symmetric mapping, and the like. The proof theory for GAPs in Section 4 does not depend on these assumptions.

Definition 7 (Satisfaction) Suppose I is a general interpretation, μ ∈ T is a c-annotation in T and A is a ground atom. Then:

1. If A is a ground atom, I ⊧ A : μ if and only if μ ∈ I(A), where μ ∈ T .

2. I ⊧ ¬A : μ if and only if ¬(μ) ∈ I(A).

3. I ⊧ F_{1} & F_{2} if and only if I ⊧ F_{1} and I ⊧ F_{2}.

4. I ⊧ F_{1} ∨ F_{2} if and only if I ⊧ F_{1} or I ⊧ F_{2}.

5. I ⊧ F_{1} ← F_{2} if and only if I ⊧ F_{1} or I |̸= F_{2}.

6. I ⊧ F_{1} ↔ F_{2} if and only if I ⊧ (F_{1} ← F_{2}) and I ⊧ (F_{2} ← F_{1}).

7. I ⊧ (∀x)F if and only if I ⊧ F (x/t) for all ground terms t. Here x is an object or annotation variable and t must be of the same sort as x (i.e., either a usual ground firstorder term, or an element of T ). F (x/t) denotes the replacement of all free occurrences of x in F by t.

8. I ⊧ (∃x)F if and only if I ⊧ F (x/t) for some ground term t, where x is an object or annotation variable.^{1}

9. If F is not a closed formula, then I ⊧ F if and only if I ⊧ (∀)F, where (∀)F denotes the universal closure of F.

Definition 8 (r-Satisfaction) Suppose I is an r-interpretation, μ ∈ T is a c-annotation in T and L is a ground literal. Then:

1. If A is a ground atom, I ⊧^{r} A : μ if and only if I(A) ≥ μ.

2. I ⊧^{r} ¬A : μ if and only if ¬(μ) ≤ I(A).

The remaining cases (3) – (10) are defined in exactly the same way as for general satisfaction.

As usual, an interpretation I (or r-interpretation J) is said to be a model (resp., r-model) of a formula F if and only if I ⊧ F (resp., J ⊧^{r} F). I is a model of a set of formulas P (of a GAP, in particular) if and only if it is a model of each of the formulas in P. Also, if P is a set of formulas and ϕ is a formula, we write P ⊧ ϕ (or P ⊧^{r} ϕ) if and only if whenever I ⊧ P (resp., I ⊧^{r} P) then I ⊧ ϕ (resp., I ⊧^{r} ϕ).

In annotated logics, there are at least two different (but related) notions of negation [32, 33]. The ontological negation is close to the standard negation in predicate calculus; for annotated logics it was first studied in [32]. On the other hand, the negation defined in (2) of Definition 7 is close to the negation used in multivalued logics. For annotated logics it was first introduced in [43, 5, 7]; it was dubbed epistemic negation in [32]. One of the advantages of epistemic negation is that, given a c-annotated literal ¬A : μ, there is a c-annotation ρ = ¬(μ) such that ¬A : μ is logically equivalent to A : ρ. This type of negation is monotonic and, therefore, is more tractable. The other negation, ontological [32], defines satisfaction of negated atoms as follows: I ⊧∼ A : μ if and only if I |̸= A : μ. In this case, there is usually no ρ such that A : ρ and ∼ A : μ are logically equivalent. As a result, ontological negation is computationally more expensive. However, the primary reason for our use of epistemic negation in this paper is not computational, but the fact that the negation in Fitting’s theory of logic programming over bilattices [18] directly translates into the epistemic negation of GAPs (see Section 5.2). Also, it is easy to see that the implication, A ← B, can be expressed via ontological negation as follows: A∨ ∼ B. However, “←” is not expressible via ∨, ∧, and the epistemic negation ¬. Therefore, since the ontological negation is not used in this paper, we had to define the implication “←” separately. Properties of ontological negation are discussed in detail in [32, 33, 13].

1If t is an annotation ground term, it can be identified with a constant in T , since all annotation functions are evaluable.

The above definition tells us what the models of a GAP are. Note that if some annotation term, ζ, appears in the head of a rule A : ζ ← Body and ζ has an annotation variable, x, which does not appear as an annotation in Body, then because of the monotonicity of annotation functions (i.e. functions in the F_{i}’s) and due to the way the semantics is defined, we can replace all occurrences of x in ζ by ⊤ while preserving program equivalence (recall that x is implicitly universally quantified). Consider the following example:

Example 2 Suppose P is the following program over the unit interval [0, 1] of truth values:

p : x ← q : 0.3
q : 0.4 ←

It is easy to see that this program is model-theoretically equivalent (using either general or restricted models) to:

p : 1 ← q : 0.3
q : 0.4 ←

(recall that when T = [0, 1] then ⊤ = 1). □

Thus, we can assume without loss of generality that, in every clause, variables occurring in the annotation of the clause head also appear as annotations of the body literals. We will make this assumption throughout this paper. For the facts (clauses with an empty body) appearing in GAPs, this implies that c-annotations can always be assumed, which is done till the end of the paper.

Following the usual development of the semantics of logic programs, we associate two operators T_{P} and R_{P} with any GAP P: T_{P} maps interpretations to interpretations and R_{P} maps r-interpretations to r-interpretations. They are defined as follows:

Definition 9 Suppose I is an interpretation and A ∈ B_{L}. Then T_{P} (I)(A) = the least ideal of T containing the set {f(μ_{1},…, μ_{n}) | A : f(μ_{1},…, μ_{n}) ← B_{1} : μ_{1} & … & B_{n} : μ_{n} is in SGI(P), and I ⊧ (B_{1} : μ_{1} & … & B_{n} : μ_{n})}. It is easy to see that intersection of an arbitrary number of ideals is an ideal, and therefore for every subset S ⊆ T there is a unique least ideal containing S. Note also that T_{P} (I)(A) is a subset, not an element, of T . □

Definition 10 Suppose I is an r-interpretation and A ∈ B_{L}. Assume also that T is a complete semilattice. Then R_{P} (I)(A) = ⊔{f(μ_{1},…, μ_{n}) | A : f(μ_{1},…, μ_{n}) ← B_{1} : μ_{1} & … & B_{n} : μ_{n} is in SGI(P), I ⊧ (B_{1} : μ_{1} & … & B_{n} : μ_{n})}. □

Notice that if I is an r-interpretation (hence also an interpretation), then R_{P} (I)(A) = ⊔T_{P} (I)(A) for each atom A, where ⊔ is the least upper bound operator (we postulate that ⊔{ } = ⊥). Later we will establish a much more general result regarding the relationship between T_{P} and R_{P} that will be subsequently used in Section 5 to establish the relationship between GAPs and van Emden’s [47] and Fitting’s [18] works.

One intuition behind the ideal-theoretic definition is the following: Consider an interpretation I and a ground atom A. If there is a clause in SGI(P) with head A : μ and whose body is satisfied by I, then we may use I to “conclude” that there is a derivation of A : μ by using modus ponens. We collect all such μ’s together as a set called Γ_{P} (I)(A), say. Now, using the finitary inference rule

\frac{A : μ_{1} , A : μ_{2}}{A : ⊔\{μ_{1}, μ_{2}\}}

we may conclude in a finitary way that Γ_{P} (I)(A) should be closed under finite lubs. The main difference between R_{P} and T_{P} is that R_{P} would also allow infinite lubs to be present. It is precisely because of this finitary/infinitary distinction that T_{P} possesses some desirable properties (to be discussed shortly) that R_{P} does not possess. The question of which semantics is more intuitive depends on whether one believes that taking infinite lubs is a justified inference step. In any case, Theorem 3 below shows that for most practical purposes the two semantics yield the same results.

Theorem 1 Suppose P is a GAP, I is an interpretation and J is an r-interpretation. Then

• I is a model of P if and only if T_{P} (I) ≤ I;

• J is an r-model of P if and only if R_{P} (J) ≤ J;

• T_{P} is monotonic;

• R_{P} is monotonic.

Proof: A simple modification of the standard proof, e.g., from [35], with the use of the monotonicity property of annotated functions in F. □

In what follows, we will often use a special “least” interpretation, Δ, which assigns the empty ideal { } to every atom. In case of restricted interpretations, the least r-interpretation may not exist, unless we require T to have the least element ⊥. In the latter case, the least r-interpretation, denoted Δ_{r}, assigns ⊥ to every atom in B_{L}.

Let us define the iterations of T_{P} as follows: T_{P} ↑ 0 = Δ. If α is a successor ordinal, then T_{P} ↑ α = T_{P} (T_{P} ↑ (α − 1)); if α is a limit ordinal, then T_{P} ↑ α = ⊔_{β<α}T_{P} ↑ β. In the preceding sentence, (α−1) denotes the immediate predecessor of the successor ordinal α. The iterations of R_{P} are defined similarly with the exception that R_{P} ↑ 0 = Δ_{r}. We will see that as in “classical” logic programming, T_{P} is continuous, and the equation T_{P} ↑ ω = lfp(T_{P}) holds, but this is not always the case with R_{P}.

Theorem 2 Let P be a GAP. Then

1. T_{P} is continuous;

2. T_{P} ↑ ω = lfp(T_{P}) = the least model of P;

3. For all annotated ground atoms A : μ, P ⊧ A : μ if and only if μ ∈ T_{P} ↑ ω(A).

Proof: The only non-obvious thing is the continuity of T_{P}. The rest of the claims follow from continuity in a standard way.

To show continuity, let I_{1}, I_{2},… be a directed sequence of interpretations of P (i.e., every finite subsequence I_{i_{1}}, ..., I_{i_{k}} has an upper bound I_{l}: I_{l} ≥ I_{i_{j}}, j = 1, ..., k). We have to show that T_{P} (⊔I_{i}) = ⊔(T_{P} (I_{i})). It is easily seen from the definitions that for any set of interpretations, {J_{k}}, their least upper bound, ⊔J_{k}, is such an interpretation J that for every ground atom A, J(A) is the least ideal containing the set ∪J_{i}(A).

Since T_{P} is monotonic, T_{P} (I_{k}) ≤ T_{P} (⊔I_{i}) for all k. Since, for every A, T_{P} (⊔I_{i})(A) is an ideal, we conclude that T_{P} (⊔I_{i}) ≥ ⊔(T_{P} (I_{i})).

In the other direction, let A be a ground atom such that μ ∈ T_{P} (⊔I_{i})(A). Then there must be a strict ground instance of a rule in P of the form A : f(μ_{1},…, μ_{n}) ← B_{1} : μ_{1} & … &B_{n} : μ_{n}, where μ = f(μ_{1},…, μ_{n}) and the literals B_{j} : μ_{j} are satisfied by ⊔I_{i}. This means that for every j = 1, ..., n, there are ν_{j1}, ..., ν_{jk_{j}} in T such that

1. each of the B_{j} : ν_{jl} is in some I_{i}; and

2. μ_{j} = ⊔{ν_{j1}, ..., ν_{jk_{j}}}.

Since the set I_{i} of interpretations is directed, there is some I_{i_{0}} that satisfies all the B_{j} : ν_{jl}. Because of (1) above, I_{i_{0}} ⊧ B_{1} : ν_{1m_{1}} & … & B_{n} : ν_{nm_{n}}, for any m_{1}, ..., m_{n} such that 1 ≤ m_{1} ≤ k_{1}, ..., 1 ≤ m_{n} ≤ k_{n}. Hence,

f(ν_{1m_{1}},…, ν_{nm_{n}}) ∈ T_{P} (I_{i_{0}})(A).  (1)

Therefore, by continuity of f (all annotation functions are continuous, by definition),

A : f(μ_{1},…, μ_{n}) =
A : f(⊔{ν_{11}, ..., ν_{1k_{1}}}, ..., ⊔{ν_{n1}, ..., ν_{nk_{n}}}) =
A : ⊔f(ν_{1m_{1}}, ..., ν_{nm_{n}}).

Thus, because of Equation (1) and since T_{P} (I_{i_{0}}), being an ideal, is closed under finite least upper bounds, we derive that f(μ_{1},…, μ_{n}) ∈ ⊔(T_{P} (I_{i}))(A), which concludes the proof. □

Corollary 1 If A is a ground atom such that μ ∈ T_{P} ↑ ω(A) then there is an integer n such that μ ∈ T_{P} ↑ n(A).

Proof: Since T_{P} ↑ n ⊆ T_{P} ↑ (n + 1) for all n ≥ 0, it follows that (T_{P} ↑ ω)(A) = ∪(T_{P} ↑ n)(A) (i.e. a plain union of sets instead of the least upper bound ⊔). Therefore μ must belong to one of the T_{P} ↑ n(A)’s. □

Unlike T_{P}, R_{P} may not be continuous, as illustrated in the following example:

Example 3 Suppose T is the interval of real numbers [0, 1] with the usual ordering, and consider the following program:

p : 0 ←
p : \frac{1+x}{2} ← p : x
q : 1 ← p : 1,

where x is an annotation variable. It is easy to see that the interpretation T_{P} ↑ i, 0 ≤ i ≤ ω, always assigns the empty ideal {} to q. Hence, (T_{P} ↑ ω)(q) = {}. Now, according to the restricted semantics,

(R_{P} ↑ ω)(p) = {a|a ≤ 1},  (2)

while according to the general semantics,

(T_{P} ↑ ω)(p) = {a|a < 1}.  (3)

Therefore, the r-semantics yields (R_{P} (R_{P} ↑ ω))(q) = T , because of the third rule, while by the general semantics we have (T_{P} (T_{P} ↑ ω))(q) = { }. This shows that R_{P} ↑ ω is not a fixpoint of R_{P} in the r-semantics; however, in the general semantics, T_{P} ↑ ω is a fixpoint of T_{P}, by Theorem 2. Notice that the only difference between Equations (2) and (3) is that “≤” is used in (2), while in (3) “<” is employed. □

Thus, we see that one of the major differences between R_{P} and T_{P} is that the latter is continuous and hence attains a fixed-point at the ω-th step of its upward iteration, while R_{P} does not possess either of these properties. Interestingly, this profound difference is merely due to the fact that we used different notions of least upper bound (of infinite sets of annotations) to define T_{P} and R_{P}. In the remainder of this section we give a simple characterization of when R_{P} attains a fixed-point at ω.

Blair and Subrahmanian [5, 7] have shown that lfp(R_{P}) = R_{P} ↑ ω whenever P is cannotated, and T is a lattice. It follows immediately from that proof that the same result holds when no annotation variables appear in rule bodies. In parallel, Kifer and Li [31] showed that lfp(R_{P}) = R_{P} ↑ ω holds at the other end of the spectrum: when P contains only vannotations in rule bodies (in which case R_{P} is even continuous). This implies that R_{P} exhibits undesirable behaviour only when c- and v-annotations are intermixed in rule bodies.

Apart from the two important cases considered in [5, 7, 31], there is a large class of programs for which R_{P} is not necessarily continuous, but still R_{P} ↑ ω = lfp(R_{P}) holds. Let us call the latter equation the fixpoint reachability requirement. Reachability of the least fixed point in at most ω iterations is important for a practical logic programming system, since otherwise it may often mean that no proof theory for the respective class of programs is likely to exist. In the following we identify a large class of programs for which the fixpoint reachability property of R_{P} holds.

First we need to introduce one additional operator, denoted ∐, that maps general interpretations to r-interpretations. Given an interpretation, J, we define (∐ J)(A) = ⊔{μ | μ ∈ J(A)}, for every atom A of B_{L}. Here ⊔ is the operator that yields the unique least upper bound of a set (assuming that ⊔{ } = ⊥). This operator will be used to establish a relationship between R_{P} and T_{P}. Its usefulness in this context becomes apparent if we recall that R_{P} (I)(A) = ⊔T_{P} (I)(A)

– a property that immediately follows from the definition.

Definition 11 A program P is acceptable if and only if the following property holds for every c-annotated literal l in the body of P:

• If ∐(T_{P} ↑ ω) ⊧ l′ for some ground instance l′ of l, then T_{P} ↑ ω ⊧ l′. □

It is easily seen that all programs whose clause bodies are either entirely c-annotated or all are v-annotated, are acceptable. In the first case, this is because (T_{P} ↑ ω) (A) is a finitely generated ideal for every atom A, and all such ideals are obviously principal. Hence ∐(T_{P} ↑ ω) = T_{P} ↑ ω. In the second case, the acceptability follows because the condition in Definition 11 is vacuously satisfied (as there are no c-annotations in the body of P).

Example 4 Consider again the program P of Example 3. Here (T_{P} ↑ ω)(p) = {a|a < 1} and thus (T_{P} ↑ ω) |̸= p : 1. On the other hand, ∐(T_{P} ↑ ω)(p) = {a|a ≤ 1} and hence ∐(T_{P} ↑ ω) ⊧ p : 1. Since p : 1 is a c-annotated literal in the body of P, P is not acceptable. □

Theorem 3 If P is acceptable and T has a least element ⊥ then

R_{P} ↑ ω = lfp(R_{P}) = the least r-model of P = ∐(lfp(T_{P})).

Surprisingly, this theorem hinges on the assumption about ⊥ as much as it does on the assumption about acceptability of P. To see this, consider a semilattice without ⊥, e.g., T = {t, f, ⊤}. Assume that t, f are incomparable to each other, but both are smaller than ⊤. Then the program {p : X ← q : X} has two minimal models: {p : t, q : t} and {p : f, q : f}, none of which is the least r-model. We thus assume the existence of ⊥ till the end of this section. Likewise, we require T to be a complete semilattice in order for R_{P} to be well-defined.

Proof of Theorem 3: By (1) of Lemma 1 below and by (1) of Theorem 2, it follows that R_{P} ↑ ω = ∐(lfp(T_{P})). By (2) of Lemma 1, R_{P} ↑ ω is a fixpoint of R_{P}; it is the least such fixpoint because of the monotonicity of R_{P} (Theorem 1). The claim about the least r-model being equal to all the rest, also easily follows from Theorem 1. □

Lemma 1 Let P be an acceptable GAP and T be a complete upper semilattice with the least element ⊥. Then

1. R_{P} ↑ ω = ∐(T_{P} ↑ ω).

2. R_{P} (R_{P} ↑ ω) = R_{P} ↑ ω.

Proof: For Claim (1), we will show that R_{P} ↑ ω ≥ ∐(T_{P} ↑ ω) and vice versa.

To see that R_{P} ↑ ω ≥ ⊔(T_{P} ↑ ω) we first prove by induction that R_{P} ↑ i ≥ T_{P} ↑ i, for all i. The base case is immediate:

T_{P} ↑ 0 = Δ ≤ Δ_{r} = R_{P} ↑ 0.

For the inductive case,

T_{P} ↑ (k + 1) = T_{P} (T_{P} ↑ k) ≤ R_{P} (T_{P} ↑ k) ≤ R_{P} (R_{P} ↑ k) = R_{P} ↑ (k + 1).  (4)

In Equation (4), the first inclusion follows because T_{P} (I)(A) ⊆ R_{P} (I)(A) for all atoms A and the second one follows by the inductive assumption and because of the monotonicity of R_{P}. We now obtain that for all k, T_{P} ↑ k(A) ⊆ R_{P} ↑ ω(A) and, finally, that R_{P} ↑ ω(A) ⊇ ⊔(T_{P} ↑ ω)(A).

In the other direction, we show that for all i,

⊔ (T_{P} ↑ ω)(A) ⊇ (R_{P} ↑ i)(A).  (5)

It would then follow that for every A,

⊔(T_{P} ↑ ω)(A) ⊇ ⊔{(R_{P} ↑ i)(A)|i = 1, 2,…} = R_{P} ↑ ω.

We prove (5) by induction on i. The base case is trivial, since Δ_{r} = ⊔Δ, by definition. For the inductive step, assume that ⊔(T_{P} ↑ ω)(A) ⊇ (R_{P} ↑ k)(A) for all A; we will show that this equality holds for k + 1 as well.

By the definition of R_{P}, R_{P} (R_{P} ↑ k)(A) = ⊔{f(μ_{1},…, μ_{n}) | A : f(μ_{1},…, μ_{n}) ← B_{1} : μ_{1} & … & B_{n} : μ_{n} is in SGI(P), R_{P} ↑ k ⊧ (B_{1} : μ_{1} & … & B_{n} : μ_{n})}. By the inductive assumption, for every such rule-instance in SGI(P), ∐(T_{P} ↑ ω) ⊧ (B_{1} : μ_{1} & … & B_{n} : μ_{n}). Because of the acceptability of P, for each i there is a sequence μ_{i}^{1} ≤ μ_{i}^{2} ≤ … such that ⊔{μ_{i}^{j} | j = 1, 2,…} = μ_{i} and (T_{P} ↑ ω) ⊧ (B_{1} : μ_{1}^{j} & … & B_{n} : μ_{n}^{j}) (acceptability is needed to ensure that logical implication holds also in cases when some of the μ_{i} are annotation constants appearing in the body of P).

Now, since annotation functions are continuous, ⊔{f(μ_{1}^{j},…, μ_{n}^{j}) | j = 1, 2,…} = f(μ_{1}, …, μ_{n}). Therefore R_{P} (R_{P} ↑ k)(A) ⊆ ⊔(T_{P} ↑ ω)(A).

For Claim (2), R_{P} (R_{P} ↑ ω) ≥ R_{P} ↑ ω follows from the monotonicity of R_{P} and since R_{P} ↑ ω ≥ R_{P} ↑ i, for all i. The other inclusion is proved similarly to the earlier proof that R_{P} (R_{P} ↑ k)(A) ⊆ ⊔(T_{P} ↑ ω)(A), in Claim (1). □

4 Constrained Queries and GAPs

Following [44], we are now going to develop an SLD-style proof theory for GAPs based on the general semantics.

Definition 12 Suppose P is a GAP and C_{1},…, C_{n} are renamed versions of clauses in P such that no pair C_{i} and C_{j} of clauses shares common variables. Further, let each C_{r}, 1 ≤ r ≤ n, be of the form

A_{r} : ρ_{r} ← B_{1}^{r} : μ_{1}^{r} & ⋯ & B_{m_{r}}^{r} : μ_{m_{r}}^{r},

where ρ_{r} is an annotation term and each μ_{k}^{r} is an annotation variable or a constant. Suppose further that A_{1},…, A_{n} are unifiable via an mgu θ and ρ = ⊔{ρ_{1}, ..., ρ_{n}}. Then the clause

[ A_{1} : ρ ← B_{1}^{1} : μ_{1}^{1} & … & B_{m_{1}}^{1} : μ_{m_{1}}^{1} & … &B_{1}^{n} : μ_{1}^{n} & … & B_{m_{n}}^{n} : μ_{m_{n}}^{n} ]θ

is called a reductant of P [32]. Here, the expression ⊔{ρ_{1}, ..., ρ_{n}} is evaluated only if all the ρ_{i}’s are c-annotations; otherwise the complex term-annotation ⊔{ρ_{1}, ..., ρ_{n}} becomes the annotation in the head of the reductant. Note, in particular, that the clauses C_{i}, C_{j} above may be different renamings of the same clause from P. Furthermore, it should be clear that each clause in P is a reductant of itself.

Example 5 Suppose T is the lattice FOUR shown in Figure 1. This lattice has been used extensively in reasoning about knowledge bases which may contain inconsistent information (cf. [6, 46]). Intuitively, ⊥ represents the Kleene’s truth value “unknown”, while ⊤ represents the truth value “inconsistent”. Let P be the program:

p(X) : t ← q(X, Y) : f
p(b) : f ← r(Z, a) : t.

Then

p(b) : ⊤ ← q(b, Y) : f, r(Z, a) : t

is a reductant of P via the mgu θ = {X\b}.

[figure: ⊤; ⊥; f; t]

Figure 1: The four-valued lattice FOUR

Theorem 4 If C is a reductant of P, then P ⊧ C.

Proof: As C is a reductant of P, it is obtained from clauses C_{1},…, C_{n}, where each C_{r} is a renamed version of a clause in P and no pair C_{i} and C_{j} shares common variables. Hence, C is of the form

(A_{1} : ρ ← B_{1}^{1} : μ_{1}^{1} & … & B_{m_{1}}^{1} : μ_{m_{1}}^{1} & … &B_{1}^{n} : μ_{1}^{n} & … & B_{m_{n}}^{n} : μ_{m_{n}}^{n})θ

where ρ = ⊔{ρ_{1}, ..., ρ_{n}}, each C_{j}, 1 ≤ j ≤ n is of the form

A_{j} : ρ_{j} ← B_{1}^{j} : μ_{1}^{j} & … & B_{m_{j}}^{j} : μ_{m_{j}}^{j},

and {A_{1},…, A_{n}} are unifiable via an mgu θ. Suppose now that I is a model of P, and Cσ is a strict ground instance of C such that

I ⊧ (B_{m_{1}}^{1} : μ_{m_{1}}^{1} & … &B_{1}^{n} : μ_{1}^{n} & … & B_{m_{n}}^{n} : μ_{m_{n}}^{n})θσ.

Hence, I satisfies the body of C_{j}θσ for all 1 ≤ j ≤ i. I is a model of P and hence a model of each C_{j} (as the C_{j}’s are only renamed versions of clauses in P). Hence, I(A_{1}θσ) ≥ ρ_{j} for all 1 ≤ j ≤ i, and thus I(A_{1}θσ) ≥ ρ = ⊔{ρ_{1},…, ρ_{i}}. This completes the proof. □

Proposition 1 Suppose P is a GAP and A : μ is an annotated atom. If P ⊧ A : μ, then there is a reductant of P having the form:

A : ρ ← B_{1} : μ_{1} & … & B_{n} : μ_{n}

such that ρ ≥ μ and P ⊧ B_{1} : μ_{1} & … & B_{n} : μ_{n}.

Proof: Suppose P ⊧ A : μ where A is a ground atom. By Theorem 2, μ ∈ T_{P} ↑ ω(A), and by Corollary 1 there is an integer k such that μ ∈ (T_{P} ↑ k)(A). We proceed by induction on k.

Base Case: k = 1. In this case, μ ∈ (T_{P} ↑ 1)(A). Hence, there are clauses C_{1},…, C_{r}, r ≥ 1, in SGI(P), of the form (empty bodies):

A : ρ_{1} ←

…

A : ρ_{r} ←

such that μ ≤ ρ = ⊔{ρ_{1},…, ρ_{r}}. Since A : ρ ← is the reductant of the above clauses, the base case follows.

Inductive Step: k = i + 1. The proof proceeds along the lines of the Base Case. □

Example 6 (S. Morishita) Suppose T is the power set of {a, b} and is ordered under inclusion. Consider the program P:

p : V ← q(X) : V
q(a) : {a} ←
q(b) : {b} ←

Clearly, P ⊧ p : {a, b}. The clause

p : ⊔{V_{1}, V_{2}} ← q(X_{1}) : V_{1} & q(X_{2}) : V_{2}

is a reductant of P involving two different renamings of the first clause. Without being able to take reductants, the proof theory given in this section would not be complete, as it would be impossible to prove p : {a, b} from P.

Definition 13 A query is a statement of the form ? − A_{1} : ρ_{1} & … & A_{k} : ρ_{k}, where the A_{i} : ρ_{i}’s are atoms annotated by a constant or a variable.^{2}

Unless explicitly stated otherwise, we will assume that queries are not necessarily c-annotated, i.e. they may contain annotation variables. If Q is a query ?− A_{1} : ρ_{1} & … &A_{k} : ρ_{k} then (∃)Q will denote the existential closure of the conjunction of its body literals, (∃) (A_{1} : ρ_{1} & … & A_{k} : ρ_{k}).

Definition 14 A constrained query Q is a statement of the form:

? − A_{1} : ρ_{1} & … & A_{k} : ρ_{k} & Constraint_{Q} ,

where

A_{1} : ρ_{1} & … & A_{k} : ρ_{k}

is the query-part of Q and Constraint_{Q} is its constraint-part. Here, each ρ_{j} is either a constant from T or an annotation variable. In the most general case, Constraint_{Q} can be any conjunction of decidable predicates^{3} over T , but in all specific theories considered in Sections 5 and 6, constraints will be of the form

τ_{1} ≥ κ_{1} & … & τ_{n} ≥ κ_{n} & α_{1} = β_{1} & … & α_{m} = β_{m},

where the τ_{i}’s, κ_{j}’s, α_{k}’s, β_{l}’s may be arbitrary term annotations (clearly, ≤ and = are decidable predicates over any lattice with a computable ⊔). □

2Notice that, as usual, a query can be viewed as a headless clause ← (A_{1} : ρ_{1} & … & A_{k} : ρ_{k}). This explains our restriction on query annotations, since only c- and v-annotations are allowed in clause bodies.

3A k-ary predicate p over T is decidable if there is an algorithm A such that for every tuple (κ_{1}, ..., κ_{k}) ∈ T^{k}, A can correctly decide whether p(κ_{1}, ..., κ_{k}) is true over T or not. In particular, we assume that constraints do not involve quantifiers.

Similarly, we can define constrained clauses of the form

A : ψ ← B_{1} : μ_{1} & … & B_{m} : μ_{m} & Constraint_{C},

which is a clause in the old sense, augmented by a constraint, Constraint_{C}. The notion of satisfaction of such clauses by an interpretation is immediate.

Definition 15 Suppose C is a constrained clause A : ψ ← B_{1} : μ_{1}& … &B_{m} : μ_{m}&Constraint_{C} and Q is a query ? − A_{1} : ρ_{1} & … & A_{k} : ρ_{k} & Constraint_{Q} such that:

1. C and Q have no (annotation or object) variables in common; and

2. A_{i} and A are unifiable via mgu θ.

Then the resolvent of Q and C with respect to A_{i} is the constrained query Q′ below:

? − [A_{1} : ρ_{1} &A_{i−1} : ρ_{i−1}& B_{1} : μ_{1} & … & B_{m} : μ_{m} & A_{i+1} : ρ_{i+1} & … & A_{k} : ρ_{k}]θ
& (Constraint_{C} & ψ ≥ ρ_{i} &Constraint_{Q}).  (6)

In the above, if θ is not required to be a most general unifier (i.e. θ is allowed to be any unifier), then Q′ is called an unrestricted resolvent of C and Q with respect to A_{i}. □

A constraint C is solvable with respect to the semilattice T and the set F of interpreted annotation functions if and only if there is an assignment σ of elements in T to the annotation variables of C, such that C has a solution with respect to T and F (Cσ is evaluated using the intended interpretation of the annotation functions in F).

There is an important class of constraints, called normal constraints, which we define next. A constraint (τ_{1} ≥ κ_{1} & … & τ_{n} ≥ κ_{n}) is normal if

1. Each κ_{i} is an annotation variable or a constant;

2. If κ_{i} is a variable, then it does not occur in τ_{1}, ..., τ_{i}.

Queries, clauses, and GAPs constrained by normal constraints are called normal queries, clauses, and GAPs, respectively.

Lemma 2 Suppose T is a lattice (not necessarily complete). Then

1. If C and Q are a normal clause and a normal query, respectively, then the resolvent of Q and C is a normal query.

2. Satisfiability of any normal constraint is decidable.

Proof: (1) Notice that ρ_{i} in Equation (6) does not appear in Constraint_{C} and in ψ, since variables have been renamed before performing the resolution step. Similarly, none of the righthand sides of inequalities in Constraint_{Q} appears in ψ. Therefore, if both Constraint_{C} and Constraint_{Q} in the above equation are normal, the constraint in the resolvent, (Constraint_{C} & ψ ≥ ρ_{i} &Constraint_{Q}), is also normal. Observe that the order of constraints in Equation (6) above is crucial.

(2) Let C be a normal constraint of the form τ_{1} ≥ κ_{1}& … &τ_{n} ≥ κ_{n}. Without loss of generality, we assume that the inequalities in C with identical variable in the right-hand side are grouped together, i.e. if κ_{i} and κ_{j} are the same variable, then for all s, i ≤ s ≤ j, κ_{s} is the same variable as κ_{i} and κ_{j}. This grouping can be achieved by the following re-grouping operation: Suppose C has a subsequence of conjuncts … &τ^{1} ≥ x& … &τ^{2} ≥ y& … &τ^{3} ≥ x. . .. Because of normality of C, x does not appear in τ^{2}, and hence the whole block of inequalities between τ^{1} ≥ x and τ^{3} ≥ x can be moved in front of τ^{1} ≥ x. Clearly, the resulting constraint will still be normal and equivalent to C. Repeating this process, we will achieve the desired grouping of conjuncts in C.

The test for satisfiability of C in T now follows:

a. If C is an empty constraint, return (satisfiable).

b. Let i_{0} ≥ 1 be the maximal integer such that κ_{i_{0}} is the same symbol as κ_{1}. Substitute ⊤ for each of the variables occurring in τ_{1}, ..., τ_{i_{0}} (the substitution must be done throughout C). Since C is normal, none of these variables appears on the right-hand side of C. Let the resulting constraint and annotation terms be also denoted by C and τ_{i}’s, respectively. Notice that now each of the τ_{1}, ..., τ_{i_{0}} can be evaluated to an element of T .

c. If κ_{1} is a constant then

If τ_{1} ≥ κ_{1}& … &τ_{i_{0}} ≥ κ_{i_{0}} is false in T

then return(unsatisfiable) /* The if-condition is verifiable since the τ_{i}’s are ground */

/* Otherwise */

Set C to τ_{i_{0}+1} ≥ κ_{i_{0}+1}& … &τ_{n} ≥ κ_{n}

Rearrange indices of the τ_{i}’s and κ_{i}’s in C so that they will start with 1, and then go to (a).

d. If κ_{1} is a variable then replace it by the greatest lower bound of τ_{1}, ..., τ_{i_{0}}, which exists since it was assumed that T is a lattice. This replacement should be done everywhere in C. Then delete the conjuncts τ_{1} ≥ κ_{1}& … &τ_{i_{0}} ≥ κ_{i_{0}} from C, as in (c), and go to (a).

Correctness of this algorithm follows immediately from the fact that all functions used in the τ_{j} in C are monotonic (see assumptions at the beginning of Section 2). Termination of the algorithm follows from the assumption that all functions in F are computable. □.

It is easy to see that the above result can be strengthened somewhat by replacing the requirement that T must be a lattice by a weaker requirement that every finite subset of T has a (not necessarily greatest) lower bound. However, then we will have to restrict C to be not only a normal constraint but also such that all conjuncts τ_{i} ≥ κ_{i}, where κ_{i} is a constant, appear in front of C. Indeed, it is easy to verify that T needs be a lattice only in step (d) of Lemma 2 and that this step will go through under the modified requirements. The next result says that if T is finite then the requirement of normality can be dropped altogether.

Lemma 3 For finite semilattices T , satisfiability of every constraint is decidable.

Proof: Suppose C is a constraint over T . Let GRD be the set of all instances of this constraint obtained by (uniformly) replacing all occurrences of annotation variables by annotation constants (in particular, constraints in GRD are free of annotation variables). As T is finite, GRD is a finite set of ground constraints (since constraints contain no quantifiers, by definition). Now, C is solvable if and only if some constraint in GRD is solvable. But for ground constraints satisfaction is obviously decidable since they are conjunctions of ground atoms involving decidable predicates only. □

Of course, the algorithm of Lemma 3 is impractical and we just used it as a decidability argument; efficient algorithms for constraint solving over T are presented in [22].

Definition 16 A deduction of a constrained query Q_{0} from a GAP P is a sequence:

Q_{0}, ⟨C_{0}, θ_{0}⟩, Q_{1},…, Q_{n}, ⟨C_{n}, θ_{n}⟩, Q_{n+1}

such that:

1. Q_{i+1} is a resolvent of Q_{i} and C_{i} via mgu θ_{i}; and

2. C_{i} is a reductant of P that contains no variables in common with Q_{i}.

When the θ_{i}’s in the above deduction are required to be unifiers but not necessarily mgu’s (i.e. the Q_{i}’s, i ≥ 1, are only required to be unrestricted resolvents), then the above deduction is called an unrestricted deduction.

Definition 17 The deduction ℜ = Q_{0}, ⟨C_{0}, θ_{0}⟩, Q_{1},…, Q_{n}, ⟨C_{n}, θ_{n}⟩, Q_{n+1} of the query Q_{0} from P is a refutation if and only if

1. Q_{n+1}, the resolvent of Q_{n} and C_{n}, has an empty query-part (i.e., Q_{n+1} is just a constraint); and

2. Q_{n+1} is solvable with respect to the lattice T and the set of annotation functions F.

In what follows, we will use SOL(ℜ) to denote the set of solutions of the constraint-part of Q_{n+1}.

Unrestricted refutation is defined similarly (where “deduction” must be replaced by “unrestricted deduction”).

The implementation of the above refutation procedure hinges upon two things:

• The ability to solve lattice constraints; and

• The ability to restrict the choice of reductants.

Studying the ways of solving constraints is beyond the scope of this paper; [22] deals with efficient serial and parallel algorithms for this task. The need to use reductants of P rather then just the clauses of P is another major obstacle. Indeed, the main appeal of SLD-resolution is that the choice of clauses that need to be considered is restricted to the current goal and the program clauses. However, if reductants are to be used, one may generate an infinite number of them out of a finite set of program clauses. Therefore, for GAPs, SLD-resolution with reduction is no better than the general resolution. Fortunately, for a large class of semilattices, we can effectively limit the number of reductants to be considered in refutations.

Definition 18 An upper semilattice T is n-wide if for every finite^{4} set E ∈ T , there is a finite subset E_{0} ⊆ E of at most n elements such that ⊔E_{0} = ⊔E. A n-reductant of a program P is a reductant involving no more than n clauses of P.

Many popular semilattices have finite width. Clearly, all finite semilattices are of this kind. Among the infinite ones, the semilattice of the form [0, 1]^{n} has width n (here (a_{1}, ..., a_{n}) ⊔ (b_{1}, ..., b_{n}) = (a_{1} ⊔ b_{1}, ..., a_{n} ⊔ b_{n})). In particular, [0, 1] and [0, 1]^{2} are frequently used in expert systems. To show that, e.g., [0, 1]^{2} is 2-wide, let α_{1} = [a_{1}, b_{1}], ..., α_{k} = [a_{k}, b_{k}] be a finite set of pairs of real numbers in the interval [0, 1]. Let a_{i} (resp., b_{j}) be the maximal element among the a_{1}, ..., a_{k} (resp., b_{1}, ..., b_{k}). Then, α_{i} ⊔ α_{j} = ⊔{α_{1}, ..., α_{k}}, which proves that [0, 1]^{2} is 2-wide.

As we shall see, if T is n-wide, then in building refutations it suffices to consider n-reductants only. This limits the choice of clauses to resolve with to a finite set of n-reductants.

Theorem 5 (Soundness) Suppose P is a GAP and Q is a constrained query such that

Q_{0}, ⟨C_{0}, θ_{0}⟩, Q_{1},…, Q_{n}, ⟨C_{n}, θ_{n}⟩, Q_{n+1}

is a refutation of Q_{0} from the GAP P. Let σ be any solution for the constraint-part of Q_{n+1}. Then Q_{0}σ is an annotation-variable-free query obtained by replacing all annotation variables in Q_{0} by the annotation constants specified in σ. We claim that:

P ⊧ (∀)(Q_{0}σ)θ_{0}θ_{1} ⋯ θ_{n}

(recall that (∀)Q_{0} denotes a conjunction of body literals of query Q_{0}, universally quantified).

Proof: We proceed by induction on n, the length of the refutation of Q_{0} from P.

Base Case: n = 1. Then Q_{0} contains exactly one annotated atom, denoted A : μ. Hence, C_{0} is of the form

D_{0} : ρ_{0} ←

such that Aθ_{0} = D_{0}θ_{0} and the constraint (ρ_{0} ≥ μ) is solvable. Let σ be any solution of this constraint and let I be a model of P. Then I is a model of C_{0} (as P entails all its reductants) and, in particular,

I ⊧ (∀)(D_{0} : ρ)

where ρ is obtained from ρ_{0} by instantiating all annotation variables to ⊤, the top element of T . In particular,

I ⊧ (∀)A_{0}θ : ρ

and as ρ = ρ_{0}σ ≥ μσ (due to the monotonicity of annotation functions in F), it follows that

I ⊧ (∀)Aθ_{0} : μ.

Inductive Step: n > 1. In this case,

Q_{1}, ⟨C_{1}, θ_{1}⟩, Q_{2},…, Q_{n}, ⟨C_{n}, θ_{n}⟩, Q_{n+1}

is a refutation of Q_{1}, where the body of Q_{n+1} is a pure constraint. Let σ be any solution of the constraint-part of Q_{n+1}. Suppose Q_{0} is

? − A_{1} : μ_{1} & … & A_{k} : μ_{k} & Constraint_{Q_{0}}.

4Finiteness is crucial here; we do not care if infinite sets do not have the property described in this definition.

If C_{0} is of the form

A : ρ ← B_{1} : ρ_{1} & … & B_{r} : ρ_{r}

and Aθ_{0} = A_{i}θ_{0} (i.e. Q_{0} and C_{0} resolve on atom A_{i} : ρ_{i} ), then Q_{1} is of the form:

? − A_{1} : μ_{1} & … & A_{i−1} : μ_{i−1} & B_{1} : ρ_{1} & … & B_{r} : ρ_{r}&A_{i+1} : μ_{i+1} & … & A_{n} : μ_{n}
& (Constraint_{Q_{0}} & ρ ≥ μ_{i}).

By the inductive hypothesis, we may assume that

P ⊧ (∀)(Q_{1}σθ_{1} … θ_{n}).

Suppose now that I is a model of P. Then, as

I ⊧ (∀)(Q_{1}σθ_{1} … θ_{n}),  (7)

it follows that

I ⊧ (∀)(B_{1} : ρ_{1}σ & … & B_{r} : ρ_{r}σ)θ_{1} … θ_{n}.

Hence, since I ⊧ C_{0} (as C_{0} is a reductant of P):

I ⊧ (∀)Aθ_{1} … θ_{n} : ρσ.

As Aθ_{0} = A_{i}θ_{0}, we conclude that:

I ⊧ (∀)A_{i}θ_{0} … θ_{n} : ρσ.

Recall that the constraint-part of Q_{1} (and hence of Q_{n+1}) contains the constraint ρ ≥ μ_{i}. As σ is a solution of the constraint Q_{n+1}, it follows that ρσ ≥ μ_{i}σ holds true in T . Thus,

I ⊧ (∀)A_{i}θ_{0} … θ_{n} : μ_{i}.

Finally, this and (7) imply

I ⊧ (∀)Q_{0}σθ_{0} ⋯ θ_{n},

which completes our proof. □

Lemma 4 (Mgu Lemma) Suppose P is a GAP and Q is a query. Suppose there is an unrestricted refutation ℜ of Q such that σ ∈ SOL(ℜ) (SOL was defined in Definition 17). Then there is a refutation ℜ′ of Q such that σ ∈ SOL(ℜ′).

Proof: Similar to the proof of the mgu lemma in classical logic programming (Lloyd, [35]). □

Lemma 5 (Lifting Lemma) Suppose P is a GAP and Q is a normal query. Suppose σ is an assignment of c-annotations to some (not necessarily all) annotation variables in Q and let θ be a substitution for object variables. If there is a refutation ℜ of Qσθ from P, then there is a refutation ℜ′ of Q from P.

Proof: Similar to the proof of the classical lifting lemma (cf. Lloyd [35]). □

Theorem 6 (Completeness Theorem) Suppose that T is a lattice, P is a GAP and Q is a normal query. Suppose P ⊧ (∃)Q. Then there is a refutation of Q from P. Moreover, if T is n-wide then Q can be refuted solely using n-reductants of P.

Proof: Suppose Q is

? − A_{1} : μ_{1} & … & A_{k} : μ_{k} & C_{Q},

where C_{Q} is the constraint-part of Q. As P ⊧ (∃)Q, it follows from Theorem 2 that T_{P} ↑ ω ⊧ (∃)Q and hence, there is an integer n such that T_{P} ↑ n ⊧ (∃)Q. We first proceed by induction on n to show that there is an unrestricted refutation of Q from P.

Base Case: m = 1. In this case, k = 1 and there is a reductant C of P of the form:

A_{1} : ρ ←

such that the constraint C_{1} ≡ (C_{Q} & ρ ≥ μ_{1}) is solvable. Hence, Q, ⟨C, θ⟩, Q_{1}, where Q_{1} is the goal ? − C_{1}, is an unrestricted refutation of Q from P.

Inductive Step: m = n + 1. Suppose now that T_{P} ↑ (n + 1) ⊧ (∃)Q. In particular, there is a variable-free instance Qσθ of Q (here, σ is an assignment of c-annotations to annotation variables and θ is a ground substitution for object variables) such that T_{P} ↑ (n + 1) ⊧ Qσθ. By the definition of T_{P} (Definition 9), this implies that for each 1 ≤ i ≤ k, there is a reductant of P, denoted C_{i}, having a ground instance of the form

A_{i} : ρ_{i} ← B_{1}^{i} : ψ_{1}^{i} & … & B_{r_{i}}^{i} : ψ_{r_{i}}^{i}

such that T_{P} ↑ n ⊧ (B_{1}^{i} : ψ_{j}^{i} & … & B_{r_{i}}^{i} : ψ_{r_{i}}^{i}) and (ρ_{1} ≥ μ_{1}& … &ρ_{k} ≥ μ_{k} & C_{Q}) is solvable.

Furthermore, if T is n-wide, then we can choose each C_{i} above to be a n-reductant. Indeed, in Definition 9, in order to obtain T_{P} (I)(A) one needs to take all possible finite least upper bounds of the elements of the set

{f(μ_{1},…, μ_{n}) | A : f(μ_{1},…, μ_{n}) ← B_{1} : μ_{1} & … & B_{n} : μ_{n} is in SGI(P), and
I ⊧ (B_{1} : μ_{1} & … & B_{n} : μ_{n})},

which amounts to taking all possible reductants of SGI(P). However, if T is n-wide, one only needs to take least upper bounds of up to n elements of the above set, which amounts to taking n-reductants only.

As C_{Q} is normal, and as annotation variables are renamed prior to resolution, (ρ_{1} ≥ μ_{1}& … &ρ_{k} ≥ μ_{k} & C_{Q}) is a normal query. Hence, for all 1 ≤ i ≤ k and for all 1 ≤ j ≤ r_{i}, we may assume, by the induction hypothesis, that there is an unrestricted refutation, denoted ℜ_{j}^{i} of B_{j}^{i} : ψ_{j}^{i}. Then, the k resolution steps that involve Q and the clauses C_{1},…, C_{k} above, followed by

ℜ = ℜ_{1}^{1}ℜ_{2}^{1} … ℜ_{r_{1}}^{1} … ℜ_{1}^{k}ℜ_{2}^{k}… ℜ_{r_{k}}^{k}

is an unrestricted refutation of Qσθ from P. By the Lifting Lemma, there is an unrestricted refutation of Q from P. This completes the proof of the inductive step.

Thus, we know that there is an unrestricted refutation of Q from P. By the Mgu Lemma, it now follows that there is a refutation of Q from P. □

It should be noted that there is no similar completeness result for r-entailment, even in the case of acceptable GAPs.

Example 7 Consider the following program P:

p : 0
p : \frac{x+1}{2} ← p : x

The query ? − p : 1 cannot be refuted by the above proof procedure, even though P ⊧^{r} p : 1. Notice that P |̸= p : 1 and so this argument is applicable to the restricted semantics but not to the general one. □

In fact, Example 7 shows that Herbrand’s theorem does not hold for r-entailment even for acceptable GAPs, which indicates that there is no sufficiently general proof procedure for the restricted semantics.

We see that there is a close relationship between annotated logic programming and constraint logic programming [30]. As will be shown later, there is also a close connection between annotated programs and certain fragments of temporal logics. Thus, there is hope that in the future a single unifying framework for multivalued, temporal, and constraint logic programming will emerge.

In related works, Morishita [36] and Subrahmanian [44] have also studied multivalued logic programming where annotations were associated with clauses, rather than with individual atoms. Morishita’s framework is as follows: Associated with each atom is a lattice, and associated with each clause is a function that maps the product of the lattices associated with the atoms in the body of the clause to the lattice associated with the head. Soundness of the proof procedure is established for queries that have a finite AND/OR tree associated with them (cf. [36, Theorem 4.11]). This restriction is not needed in our work. It must also be pointed out that our idealtheoretic semantics differs from Morishita’s semantics. Hence our completeness result applies to Example 7, whereas Morishita’s completeness result is inapplicable to that example. Results on query processing procedures for programs whose clauses are c-annotated were obtained in Subrahmanian [44] and Kifer and Lozinskii [32, 33].

5 Multivalued Logics and GAPs

The principal aim of this section is to show that quantitative logic programming as proposed by van Emden[47] and also the bilattice-based logic programs of Fitting [18], all fit into the framework of GAPs.

5.1 van Emden’s Quantitative Deduction

A quantitative rule [47] is of the form:

r : A ← B_{1} & … & B_{k},

where r ∈ (0, 1]. A quantitative rule set (QRS) is a collection of finitely many rules. Interpretations map ground atoms into the unit interval [0, 1]. Interpretations of QRSs, as defined in [47], are the same as r-interpretations of GAPs over the lattice T = [0, 1] (with the standard ordering on [0, 1]). Throughout this section, the word “interpretation” will mean “r-interpretation.”

Associated with a QRS, P, is an operator S_{P} that maps interpretations to interpretations, and is defined as follows:

S_{P} (I)(A) = ⊔{r × k | r : A ← B_{1} & … & B_{n} is a ground instance of a clause in P
and min{I(B_{1}),…, I(B_{n})} = k}.

If P is a QRS, then it can be translated into a GAP, tr(P), as follows:

tr(P) = {A : r × min{T_{1},…, T_{n}} ← B_{1} : T_{1} & … & B_{n} : T_{n} |
where r : A ← B_{1} & … & B_{n} is a clause in P }.

Note that according to this translation, all QRSs get translated into GAPs whose bodies contain only v-annotated literals. Hence, for any QRS P, tr(P) is an acceptable GAP and thus R_{tr(P)} has the fixpoint reachability property.

Theorem 7 Suppose P is a QRS. Then S_{P} = R_{tr(P)}.

Proof: The proof is a direct consequence of the definition of tr(P). □

Theorem 7 shows, in particular, that lfp(S_{P}) = lfp(R_{tr(P)}), and since tr(P) is always acceptable, we also have that lfp(S_{P}) = ∐ lfp(T_{tr(P)}).

Furthermore, for finite programs (i.e. programs with a finite set of rules and facts) we can show that ∐ lfp(T_{tr(P)}) = lfp(T_{tr(P)}). Indeed, because of the special form of their annotation functions, the rules in tr(P) never produce new annotation constants when applied in the computation of T_{tr(P)} ↑ ω. Therefore, for any atom A, (T_{tr(P)} ↑ ω)(A) will be a finitely generated ideal. Since every such ideal is principal, the ∐ operator has no effect on lfp(T_{tr(P)}). Furthermore, note that the clauses in tr(P) have empty constraint-parts and thus are normal.

As a consequence of the fact that lfp(S_{P}) = lfp(T_{tr(P)}), one can study the least model of a QRS P by studying the least model of the GAP tr(P), and the remark about normality of tr(P) in the previous paragraph implies that the proof procedure for GAPs described in the preceding section yields a sound and complete proof procedure for answering existential queries to QRS. This improves upon van Emden’s “weak soundness and completeness” results in two ways:

1. van Emden’s evaluation procedure [47] works under the conditions that the AND/OR tree associated with a program P and a query Q is finite. No such restriction is needed here.

2. van Emden’s proof procedure applies to ground queries. The procedure for GAPs described in this paper applies to non-ground existential queries as well.

Thus, the theorems about GAPs given in the previous section shed new light on the operational aspects of van Emden’s QRSs. However, unlike QRSs, GAPs are not restricted to the interval [0,1] of truth values, and the results are applicable to any multi-valued logic based on a complete lattice that possesses Henkin’s existential property.

5.2 Bilattice-valued Logics

For the purpose of this section, we assume that the reader is familiar with the basics of Fitting’s theory of bilattice-based logic programming developed in [18]. Bilattices, due to Ginsberg [23], provide an elegant epistemological framework for studying multivalued logics. Intuitively, a bilattice (also known as an interlaced bilattice) is a set ℜ having two orderings: the knowledge order, ≤_{k}, and the truth order, ≤_{t}, such that (ℜ, ≤_{k}, ⊓_{k}, ⊔_{k}) and (ℜ, ≤_{t}, ⊓_{t}, ⊔_{t}) are both complete lattices. In addition, meets and joins with respect to ≤_{k} are monotone with respect to ≤_{t} and vice versa. Fitting [17, 18] has developed a theory of fixpoints for logic programs whose associated set of truth values forms a bilattice.

In Fitting’s formulation, the syntax of a bilattice logic program is similar to that of an ordinary logic program, except that the body of a clause may be an arbitrary first order formula constructed out of ∧_{t}, ∨_{t} (“and” and “or” with respect to ≤_{t}), ∧_{k}, ∨_{k} (“and” and “or” relative to ≤_{k}), and ¬. Negation is interpreted as a unary function on truth values such that μ_{1} ≤_{k} μ_{2} if and only if ¬μ_{1} ≤_{k} ¬μ_{2}, and μ_{1} ≤_{t} μ_{2} if and only if ¬μ_{2} ≤_{t} ¬μ_{1}.

Unlike annotated clauses that essentially have a two-valued satisfaction relation, in bilatticebased logics formulae may assume any truth value from ℜ. The fundamental role of the truth order is to allow defining the logical connectives ∧_{t}, ∨_{t}, and ¬ without having to bother with specifics of the set of truth values ℜ. In contrast, the truth order plays no role in the semantics of annotated logics. The fundamental role of the knowledge order is to give meaning to logical implication, and it is used in a similar way by both annotated and bilattice-based logics. In a sense, the results of this section show that Fitting’s theory of bilattice-based logic programming uses the knowledge order in a more essential way than the truth order.

Interpretations of Fitting’s programs are the same as r-interpretations of GAPs. In other words, they are functions from Herbrand base of P to ℜ. These functions are extended to arbitrary formulas by distributing them through the connectives ∧_{t}, ∨_{t}, ∧_{k}, ∨_{t}, and ¬. Associated with a program, P, is an operator V_{P} that maps interpretations to interpretations as follows:

V_{P} (I)(A) = ⊔{μ | A ← L_{1} & … & L_{n} is a ground instance

of a clause in P and μ = I(L_{1} & … & L_{n})}.

Given a bilattice-based logic program, we can translate it into a GAP, denoted bl(P), clausewise as follows: Let C denote a clause A ← Body(L_{1}, ..., L_{n}) in P, where Body(L_{1}, ..., L_{n}) is a Fitting’s formula involving atomic literals L_{1}, ..., L_{n} (different occurrences are considered as different literals). Then the corresponding clause, bl(C), has the form

A : f_{Body(L_{1},...,L_{n})}(T_{1},…, T_{n}) ← L_{1} : T_{1} & … & L_{n} : T_{n},

where T_{1}, ..., T_{2} are annotation variables and the function f_{Body(L_{1},...,L_{n})} is defined as follows:

1. If Body(L_{1}, ..., L_{n}) = Body_{1}(L_{1}, ..., L_{k}) ∨_{t} Body_{2}(L_{k+1}, ..., L_{n}) then f_{Body}(T_{1}, ..., T_{n}) = f_{Body_{1}}(T_{1}, ..., T_{k}) ⊔_{t} f_{Body_{2}}(T_{k+1}, ..., T_{n})

2. If Body(L_{1}, ..., L_{n}) = Body_{1}(L_{1}, ..., L_{k}) ∨_{k} Body_{2}(L_{k+1}, ..., L_{n}) then f_{Body}(T_{1}, ..., T_{n}) = f_{Body_{1}}(T_{1}, ..., T_{k}) ⊔_{k} f_{Body_{2}}(T_{k+1}, ..., T_{n})

3. If Body(L_{1}, ..., L_{n}) = Body_{1}(L_{1}, ..., L_{k}) ∧_{t} Body_{2}(L_{k+1}, ..., L_{n}) then f_{Body}(T_{1}, ..., T_{n}) = f_{Body_{1}}(T_{1}, ..., T_{k}) ⊓_{t} f_{Body_{2}}(T_{k+1}, ..., T_{n})

4. If Body(L_{1}, ..., L_{n}) = Body_{1}(L_{1}, ..., L_{k}) ∧_{k} Body_{2}(L_{k+1}, ..., L_{n}) then f_{Body}(T_{1}, ..., T_{n}) = f_{Body_{1}}(T_{1}, ..., T_{k}) ⊓_{k} f_{Body_{2}}(T_{k+1}, ..., T_{n})

5. If Body(L_{1}, ..., L_{n}) = ¬Body_{1}(L_{1}, ..., L_{n}) then f_{Body}(T_{1}, ..., T_{n}) = ¬f_{Body_{1}}(T_{1}, ..., T_{k}).

In the above, ∨ and ∧ are logical connectives, while ⊔ and ⊓ are meet and join on ℜ relative to the appropriate orderings (≤_{t} or ≤_{k}). Furthermore, for the purpose of this translation, we assume that the GAP bl(P) uses the same negation operator ¬ : ℜ ⟶ ℜ as the one used by the bilattice-based program P.

Note that according to this translation, if P is a bilattice program, then bl(P) is a GAP such that all literals occurring in clause bodies are v-annotated. Hence, bl(P) is acceptable.

As mentioned earlier, the truth-order plays no role in the semantics of GAPs, while it does in the semantics of multivalued programs. However, as can be seen from the definition of bl(C), the truth-order of bilattices is encoded in the annotation functions of clauses of bl(C). This explains why GAPs can successfully simulate multivalued programs.

Theorem 8 Suppose P is a bilattice-based logic program. Then V_{P} = R_{bl(P)}.

Proof: The proof is a straightforward consequence of the translation of P into a GAP. It is clear that the annotation functions in the GAP bl(P) have been designed precisely so that they would simulate the computation of truth values for the rule heads in the bilattice-based program P. □

Since rule bodies in bl(P) are v-annotated, such programs are acceptable and we have lfp(V_{P}) = ∐ lfp(T_{bl(P)}). In general, this equality does not guarantee the existence of a complete proof theory for bilattice-based logic programs. However, for distributive bilattices such a proof procedure does exist.

A distributive bilattice [18] is a bilattice satisfying all twelve distributive laws for various combinations of the operators ⊔_{k}, ⊔_{t}, ⊓_{k}, and ⊓_{t}.

Now, as in the case of van Emden’s QRSs, finite programs will result in only a finite number of annotations being mentioned in bl(P). Since in a distributive bilattice one can always convert any expression involving ⊔_{k}, ⊔_{t}, ⊓_{k}, and ⊓_{t} into a normal form (e.g., a disjunctive normal form with k-operators inside and t-operators outside), such expressions can yield only a finite number of annotation constants, given a finite number of such constants as an input. Therefore, arguing as in the previous subsection, we conclude that ∐ has no effect on lfp(T_{bl(P)}), i.e. lfp(V_{P}) = lfp(T_{bl(P)}). Furthermore, as with QRS, we can observe that constraints arising in bl(P) are normal and therefore the proof procedure developed for GAPs applies.

As a consequence, once again, just as in the case of van Emden’s QRSs [47], we can study the semantics of bilattice logic programming by studying the semantics of the corresponding GAPs, and we can use the corresponding proof procedure to answer queries. There are several advantages in doing so:

1. Fitting did not define the notion of a model for his logic programs. However, when bilatticebased logic programs are converted into GAPs, this notion becomes clear: I is a model of a clause C in a bilattice-based program if and only if I is an r-model of the translation of C into a generalized annotated clause (see below).

2. We can use the operational semantics of GAPs developed in the previous section to process queries to bilattice-based programs. In [19], Fitting described a tableau-based proof procedure for his logic programs. This procedure is restricted to the case of the four-valued bilattice depicted in Figure 1. Since this bilattice is distributive, our results about the proof theory subsume the corresponding results in [19].

Now, the models of Fitting’s logic programs can be defined as follows:

Definition 19 We say that I is a model of a ground clause

A ← Body

in a bilattice-based program if and only if I(A) ≥_{k} I(Body). I is a model of a nonground such a clause, C, if and only if I is a model of each ground instance of C. As usual, I is a model of a bilattice-based logic program, P, if and only if I is a model of each clause in P.

Theorem 9 Let I be an interpretation of a bilattice-based program P. Then I is a model of P if and only if V_{P} (I) ≤ I if and only if I is an r-model of bl(P). □

As a consequence of the last two theorems, the models of a bilattice logic program P are also the models of the GAP bl(P), and their least models coincide. Thus, bilattice model theory can be studied through the model theory of GAPs. Moreover, in the case of finite databases and distributive bilattices, processing of existential queries to bilattice logic programs can be converted into the equivalent problem of processing existential queries for GAPs.

There is at least one intriguing result due to Fitting that does not fit in our framework. This is the elegant theorem that states the connection between the least fixed-point of V_{P} relative to the ≤_{k} ordering, and the greatest fixed-point of the V_{P} operator in the ≤_{t} ordering. This result cannot be obtained in the GAP framework simply because our formalization assumes only one ordering on T , namely ≤_{k}.

6 Temporal Reasoning

There are several different kinds of temporal logics. One of the fundamental differences of opinion between temporal logicians concerns the issue of the nature of time. Various representations of time are possible – each representation is accompanied by a host of philosophical and epistemological arguments. Here, we will consider two widely accepted representations:

1. Linear time stretching either finitely or infinitely back.

2. Interval-based time where one considers “time periods.” rather than “time points”

6.1 Reasoning about Linear Time using GAPs

Let us assume that Z is the set of all integers and that Y is some subset of Z that is upward closed under ≤, i.e. if x ∈ Y and x ≤ y, then y ∈ Y. Thus, Y may be Z itself (in which case we are assuming that the world has been around infinitely long) or Y may be, say, the set of all non-negative integers (in which case we are subscribing to the theory that the world was created at some time). So, in any case, let us assume that Y is fixed.

A temporal Herbrand interpretation I assigns a truth value to a ground atom, A, at each time point. Thus, I may say that A is true at times 1, 3, 5,… and false at times 2, 4, 6,. . .. Intuitively, we may view an interpretation I as a mapping from the Herbrand Base, B_{L}, of our language L, to the power set, P(Y), of Y. The epistemic interpretation of this is as follows:

A is true at time t according to interpretation I if and only if t ∈ I(A).

Now we can reason about time in the framework of GAPs by taking as our set T of truth values, the set P(Y) ordered by subset inclusion. Given any truth value μ, i.e. μ is a subset of Y, define an annotation function succ as follows:

succ(μ) = {t + 1 | t ∈ μ}.

Thus, if proposition p is assigned μ by interpretation I, i.e. interpretation I says that p is true at all those times in μ, and if I assigns succ(μ) to q then I says that q is true at a time point (t + 1) if p is true at time point t. For instance, the clause

get out of way : succ(μ) ← see car coming : μ

says that if you see a car coming at you at a certain moment then get out of its way at the next time moment. To say that p is true at all even times, we write

p : {0} ←
p : succ(succ(α)) ← p : α.

Baudinet [3] has developed a semantic framework for temporal logic programming, with Y taken to be the set of non-negative integers. According to this framework, a temporal logic program can be considered as a (possibly infinite) set of clauses of the form:

C : ◯^{i_{0}}A_{0} ← ◯^{i_{1}}A_{1} & … & ◯^{i_{n}} A_{n},

where ◯ is the modal operator next and ◯^{j} is a shorthand for j applications of ◯. If A is an atom and i ≥ 0, then ◯^{i}A is called a next-atom. An interpretation is just a collection of ground next-atoms.

The above clause C can be translated into the following c-annotated clause an(C):

A_{0} : {i_{0}} ← A_{1} : {i_{1}}& … &A_{n} : {i_{n}} .

For a temporal program, P, an(P) = {an(C)| C ∈ P }.

To compare GAPs with [3], let Y be the set of all non-negative integers {0, 1,…}, and T = P(Y) be the lattice of all sets of non-negative integers ordered by inclusion, which we call the temporal lattice. Thus, for instance, Baudinet’s interpretation {◯ ◯ A} that says that A is true at time 2 and all other propositions are false at all times is captured by our multivalued interpretation I defined as:

I(A) = {2} and for all B ≠ A, I(B) = { }

Formally, let I be a collection of Baudinet’s next-atoms. The translation of I into an rinterpretation, an(I), for annotated logic is:

(an(I))(A) = {i | ◯^{i} A ∈ I}.

Baudinet then defines an operator, denoted Z_{P}, that maps sets of ground next-atoms to sets of ground next-atoms as follows:

Z_{P} (I) = {◯^{i}A | ◯^{i} A ← B_{1} & … & B_{n} is a ground instance
of a clause in P and {B_{1},…, B_{n}} ⊆ I}.

Likewise, in the context of annotated logics, we may consider the R_{an(P)} operator defined on GAPs:

Theorem 10 For any temporal program, P, and a Baudinet’s interpretation, I,

an(Z_{P} (I)) = R_{an(P)}(an(I)). □

The above theorem establishes that one way of studying Baudinet’s temporal logic programming is within the framework of GAPs. For instance, as in Section 5, we can argue that for finite programs R_{an(P)} = T_{an(P)} and this allows us to use the theorems in Section 4 to define a proof procedure for answering existential queries to temporal programs.

A more expressive temporal logic was proposed by Abadi and Manna in [1]. There, besides the “next” operator, ◯, other modalities, such as “eventuality”, ◇, and “always true”, □, are allowed. The full temporal logic of [1] is, according to the authors, computationally expensive, and a fragment amenable to an efficient implementation by means of SLD resolution was proposed. This fragment consists of clauses of the following form. First, rule bodies are drawn from the class of formulas, B, which contains all next-atoms, and is closed under conjunction and under the application of ◇. The initial clauses, i.e., clauses that are true at time 0 are of the form

1. B ← A; or

2. □B ← A,

where A ∈ B and B is a next-atom. The permanent clauses, i.e., rules that are always true, have the form □(B ← A), where, as before, A ∈ B and B is a next-atom.

Let Y and T be the same as before. We have already shown how the next-atoms are represented using annotations. The necessity operator, □, corresponds to the topmost element ⊤ ∈ T (which represents the whole set Y). For instance, □A is represented as A : ⊤. Finally, our annotated rules correspond to the permanent rules of [1].

We show below some simple examples of information that can be represented using the GAP formalism. Suppose in the sequel that Y is the set of all integers. For example, to say that if X is a president at time T, then X must have been rich at time (T − 1) (think of time units as “years”), we can say:

rich(X) : previous(μ) ← president(X) : μ,

where

previous(μ) = {t − 1 | t ∈ μ}

is an annotation function. In TEMPLOG ([1]), we could express this as:

□(rich(X) ← ◯president(X)).

The statement: “if sometime she becomes a president then she must be rich” is written as

□(rich(X) ← ◇president(X))

in TEMPLOG, and as

rich(X) : {0} ← president(X) : μ

in our logic.

On the other hand, the statement “if X is a life-long president, then X is a ruthless murderer”, written as

□(murderer(X) ← □president(X))

in temporal logic, is not allowed in TEMPLOG. In contrast, representing this as a GAP is straightforward:

murderer(X) : ⊤ ← president(X) : ⊤.

In general, since we allow arbitrary computable functions (subject to the restrictions of Section 4) in rule heads while both Baudinet and Abadi and Manna restrict the rule heads to be next-atoms (i.e. c-annotated literals, in our setting), GAPs can express several fancy temporal problems that are beyond the scope of [1, 3]. Also, we do not restrict bodies of temporal programs to be □-free, since atoms of the form A : ⊤ are perfectly acceptable.

There are, however, situations where GAPs are weaker than [1]. For instance, GAPs cannot express a clause with the following body: ◇(p ∧ ◇q). Likewise, we cannot represent directly the initial clauses of Abadi and Manna, since GAP rules are permanently true.

This difficulty could be overcome by using metaprogramming techniques (e.g. [45]). In these formalisms, formulae can be encoded by terms, and thus can be reasoned about. For instance, if < B ← A > is an encoding of a clause B ← A, then we could write clause(< B ← A >) : {0}, stating that the respective clause is true at time 0, which corresponds to the initial clause B ← A of [1]. We will not discuss this issue any further in this paper. More information about encodings and logics for meta-reasoning can be found in [14, 37, 38, 27, 45].

6.2 Multivalued Temporal Reasoning

One advantage of the GAP formalism as opposed to Baudinet’s and Abadi and Manna’s is that it also allows one to deal with “epistemically inconsistent worlds”, i.e. interpretations in which at certain times t the information about certain ground atoms is inconsistent. More generally, assume that now our domain of truth values is the set of functions from Y to some complete lattice T′, i.e.

T = (Y → T′).

For instance, we can take T′ to be the four-valued Belnap’s lattice [4] shown in Figure 1, or we can take T′ to be the set [0, 1] × [0, 1] often used for modeling uncertainty in expert systems [7, 31, 18]. An interpretation is a map from B_{L} to T . The underlying intuition is that an interpretation I assigns to any ground atom A, a function f_{A} from Y to T′. If T′ is the fourvalued Belnap’s lattice of Figure 1, and f_{A}(3) = ⊤, f_{A}(4) = t then we can think of this as an assertion that at time 3, A was inconsistently defined, but at time 4 it became true.

6.3 Interval Based Temporal Logic

Let us assume that time is linearly represented by the set of all non-negative integers. In an interval based temporal logic, we can use closed intervals of integers as truth values. We use the notation:

[a, b] = {n | a ≤ n ≤ b}.

Let ℜ be the set

ℜ = {[a, b] | a ≤ b and a, b are non-negative integers}.

The intervals in ℜ are partially ordered by inclusion and we denote this ordering by ≤_{ℜ}. Let us take T to be the set of subsets of ℜ such that every α ∈ T satisfies the following two properties:

1. If [a, b] ∈ α and [c, d] ⊂ [a, b] then [c, d] ∈ α;

2. If [a, b] ⊂ ∪α, where ∪α is the union of all intervals in α, then [a, b] ∈ α.

Intuitively, assignment of a set α = {[a_{1}, b_{1}],…, [a_{j}, b_{j}],…} to an atom A by an interpretation I means that A is true in each of the intervals [a_{j}, b_{j}]. This epistemic interpretation of elements of T makes the above conditions self-explanatory: if an event takes place over a time interval then it also takes place over a subinterval; if an event takes place over a group of time intervals then this event also takes place over any interval that is covered by the group. In fact, it is easy to see that the second condition above implies the first one.

There exist several popular orderings of power-domains over partial orders. The one that is particularly useful to model time is the following: for α, β ∈ T , α ≤_{T} β if and only if for every interval ı ∈ α there exists an interval ȷ ∈ β such that ı ≤_{ℜ} ȷ.

To see that GAPs can represent some forms of interval temporal reasoning, we show that the logic of Shoham [42, pp. 61–62] can be expressed within the GAP framework. Shoham extends classical propositional logic to an interval modal logic by adding six new modal connectives as follows:

1. ⟨A⟩ is true in the interval [t_{1}, t_{2}] if and only if there exists t_{2} < t_{3} (here < denotes the regular order on integers) such that p is true in the interval [t_{2}, t_{3}]. Intuitively, modality ⟨A⟩ represents the intuition that p is true in some interval immediately following the current interval.

2. ⟨B⟩p is true in [t_{1}, t_{2}] if and only if there exists a t_{3} such that t_{1} ≤ t_{3} < t_{2} and p is true in the interval [t_{1}, t_{3}]. Intuitively, ⟨B⟩ represents the idea that p is true in some subinterval of the current interval that starts at the same time as the current interval.

3. ⟨E⟩p is true in the interval [t_{1}, t_{2}] if and only if there is a t_{3} such that t_{1} < t_{3} ≤ t_{2} and p is true in the interval [t_{3}, t_{2}]. In other words, ⟨E⟩p becomes true earlier than p and remains true while p was true.

4. ⟨\overline{A}⟩p is true in [t_{1}, t_{2}] if and only if there exists a t_{3} such that t_{3} < t_{1} and p is true in the interval [t_{3}, t_{1}]. Here ⟨\overline{A}⟩ means that p is true at some interval ending immediately before the current interval starts.

5. ⟨\overline{B}⟩p is true in the interval [t_{1}, t_{2}] if and only if there exists a t_{3} such that t_{2} < t_{3} and p is true in [t_{1}, t_{3}]. Intuitively, the ⟨\overline{B}⟩ modality represents the intuition that p is true in some interval of which the current interval is the beginning.

6. ⟨\overline{E}⟩p is true in the interval [t_{1}, t_{2}] if and only if there exists a t_{3} such that t_{3} < t_{1} and p is true in [t_{3}, t_{2}]. Intuitively, the ⟨\overline{E}⟩ modality represents the intuition that p is true in some interval of which the current one is the end.

Given any n-ary predicate symbol p, we can express these six modalities as GAPs by using the following clauses:

p_{⟨A⟩}(X_{1},…, X_{n}) : α ← p(X_{1},…, X_{n}) : β & end(α) = start(β) & end(α) < β. p_{⟨B⟩}(X_{1},…, X_{n}) : α ← p(X_{1},…, X_{n}) : β & start(α) = start(β) & β < α. p_{⟨E⟩}(X_{1},…, X_{n}) : α ← p(X_{1},…, X_{n}) : β & end(α) = end(β) & β < α. p_{⟨\overline{A}⟩}(X_{1},…, X_{n}) : α ← p(X_{1},…, X_{n}) : β & end(β) = start(α) & end(β) < α. p_{⟨\overline{B}⟩}(X_{1},…, X_{n}) : α ← p(X_{1},…, X_{n}) : β & start(α) = start(β) & α < β. p_{⟨\overline{E}⟩}(X_{1},…, X_{n}) : α ← p(X_{1},…, X_{n}) : β & end(α) = end(β) & α < β.

In the above, X_{1},…, X_{n} are object variables and α, β are annotation variables. Annotation functions end and start are defined as follows:

start(α) = {[a, a]| [a, b] is a maximum interval in α};
end(β) = {[b, b]| [a, b] is a maximum interval in β}.

An interval [a, b] ∈ α ∈ T is maximum if it is not properly contained in another interval in α. Also note that satisfiability of constraints in the above clauses is decidable since this is a very simple case of linear programming, and thus the proof theory for GAPs applies.

The above translation precisely captures the intended meaning of the modal operators of Shoham [42] but, in general, we cannot simulate full-fledged interval-based temporal logics. This, of course, does not come as a surprise, since even the propositional temporal logic ITL has an undecidable validity problem [25].

7 Conclusions

There are many alternative formalisms for multivalued and temporal logic programming. However, the relationship between these different formalisms is not well understood. In this paper, we have made a first contribution towards the understanding of different methodologies for logic programming based on non-standard logics.

We have shown that annotated logics can serve as common grounds for several of the multivalued and temporal formalisms. Besides the theoretical interest, this has numerous practical benefits. First, already known results about GAPs can be used to obtain a direct characterization of certain kinds of temporal reasoning. Second, GAPs can be used to identify semi-decidable fragments of temporal logics by translating them into GAPs, as suggested in this paper (recall that the implication problem for GAPs is recursively enumerable). This is important because, we believe, logics with non-recursively enumerable implication problem cannot be effectively implemented on a computer. Third, it gives a proof theory to formalisms based on multivalued logics, such as [47, 18], which can be naturally translated into GAPs. Finally, when all else fails, one may prefer to program in terms of GAPs directly rather than using different formalisms (subsumed by GAPs) for different purposes.

Acknowledgements. We thank Mel Fitting, and Raymond Ng for useful suggestions on preliminary versions of this paper. S. Morishita pointed out to a mistake in an earlier version of Theorem 6. We are also grateful to the anonymous referees for many helpful suggestions.

References

[1] M. Abadi and Z. Manna. (1987) Temporal Logic Programming, Proc. 4th IEEE Symp. on Logic Programming, pp 4–16, Computer Society Press.

[2] K. R. Apt, H. A. Blair and A. Walker. (1988) Towards a Theory of Declarative Knowledge, in: Foundations of Deductive Databases and Logic Programming, (ed. Jack Minker), Morgan-Kauffman.

[3] M. Baudinet. (1989) Temporal Logic Programming is Complete and Expressive, Proc. of the ACM Conference on Principles of Programming Languages, Austin, Texas.

[4] N.D. Belnap. (1977) A Useful Four-Valued Logic, in G. Epstein and J.M. Dunn, eds. Modern Uses of Many-valued Logic, (eds. G. Epstein and J.M. Dunn), D. Reidel, pp. 8-37.

[5] H. A. Blair and V.S. Subrahmanian. (1989) Paraconsistent Logic Programming, Theoretical Computer Science, 68, pp 135–154.

[6] H. A. Blair and V. S. Subrahmanian. (1988) Strong Completeness Results for Paraconsistent Logic Programming, submitted.

[7] H. A. Blair and V. S. Subrahmanian. (1988) Paraconsistent Foundations for Logic Programming, Journal of Non-Classical Logic, 5, 2, pp 45–73.

[8] L. Farinas del Cerro. (1986) Molog: A System That Extends Prolog with Modal Logic, New Generation Computing.

[9] N.C.A. da Costa. (1974) On the Theory of Inconsistent Formal Systems, Notre Dame J. of Formal Logic, 15, pp. 497–510.

[10] N.C.A. da Costa and E.H. Alves. (1977) A Semantical Analysis of the Calculi C_{n}, Notre Dame J. of Formal Logic, 18, pp. 621-630.

[11] N.C.A. da Costa and E.H. Alves. (1981) Relations between Paraconsistent Logic and Manyvalued Logic, Bulletin of the Section of Logic, 10, pp. 185-191.

[12] N.C.A. da Costa, L. J. Henschen, J. J. Lu and V.S. Subrahmanian. (1989) Automatic Theorem Proving in Paraconsistent Logics: Theory and Implementation, in: Proc. 10th International Conference on Automated Deduction, Lecture Notes in Computer Science Vol. 449, pp. 72–86, July 1990.

[13] N.C.A. da Costa, V.S. Subrahmanian and C. Vago. (1989) The Paraconsistent Logics PT , to appear in: Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik, Vol. 37, 1991.

[14] S. Feferman. (1984) Toward Useful Type-Free Theories, Journal of Symbolic Logic, 49, pp. 75-111.

[15] M. C. Fitting. (1987) Bilattices and the Theory of Truth, to appear in: Journal of Philosophical Logic.

[16] M. C. Fitting. (1987) Enumeration Operators and Modular Logic Programming, Journal of Logic Programming, 4, pp. 11–21.

[17] M. C. Fitting. (1988) Logic Programming on a Topological Bilattice, Fundamenta Informaticae, 11, pp. 209–218.

[18] M. C. Fitting. (1991) Bilattices and the Semantics of Logic Programming, Journal of Logic Programming, 1991. to appear.

[19] M. C. Fitting. (1989) Negation as Refutation, Proc. 4th Symp. on Logic in Computer Science, Asilomar, CA, pp. 63-70.

[20] D. M. Gabbay. (1987) Modal and Temporal Logic Programming, in: Temporal Logic in Computer Science, (ed. A. Galton), Academic Press.

[21] A. Galton. (1987) Temporal Logic in Computer Science, Academic Press.

[22] D.D. Ganguly and S. Ranka. (1990) A Space Efficient Coding Algorithm for Lattice Computations, draft manuscript.

[23] M. Ginsberg. (1988) Multivalued Logics: A Uniform Approach to Reasoning in Artificial Intelligence, Computational Intelligence, vol. 4, 1988, pp. 265–316.

[24] M. Ginsberg. (1990) Bilattices and Modal Operators, in: Proc. 1990 Intl. Conf. on Theoretical Aspects of Reasoning About Knowledge, Morgan Kaufmann.

[25] J.Y. Halpern, Z. Manna and B. Moszkowski. (1983) A High-Level Semantics Based on Interval Logic, Proc. ICALP 1983, pp 278–291, Springer.

[26] L.J. Henschen, J. J. Lu and V.S. Subrahmanian. (1989) An Improved Resolution Procedure for Paraconsistent Logics , submitted.

[27] P.M. Hill and J.W. Lloyd. (1988) Analysis of Meta-Programs, Tech. Report CS-88-08, University of Bristol, UK.

[28] M. Ishizuka. (1983) Inference Methods Based on Extended Dempster and Shafer’s Theory with Uncertainty/Fuzziness, New Generation Computing, 1, 2, pps 159–168.

[29] M. Ishizuka and N. Kanai. (1985) PROLOG-ELF Incorporating Fuzzy Logic, New generation Computing, 3, pps 479–486.

[30] J. Jaffar and J-L Lassez. (1987) Constraint Logic Programming, POPL-87, Munich, W. Germany.

[31] M. Kifer and A. Li. (1988) On the Semantics of Rule-Based Expert Systems with Uncertainty, 2-nd Intl. Conf. on Database Theory, Springer Verlag LNCS 326, (eds. M. Gyssens, J. Paredaens, D. Van Gucht), Bruges, Belgium, pp. 102–117.

[32] M. Kifer and E.L. Lozinskii. (1989) RI: A Logic for Reasoning with Inconsistency, 4-th Symposium on Logic in Computer Science, Asilomar, CA, pp. 253–262.

[33] M. Kifer and E.L. Lozinskii. (1991) A Logic for Reasoning with Inconsistency, Journal of Automated Reasoning, Kluwer Academic Publ., 1991, to appear.

[34] M. Kifer and V.S. Subrahmanian. (1989) On the Expressive Power of Annotated Logic Programs, Proc. 1989 North American Conference on Logic Programming, Cleveland, Ohio, pp. 1069–1089, MIT Press.

[35] J.W. Lloyd. (1987) Foundations of Logic Programming, Springer-Verlag.

[36] S. Morishita. (1989) A Unified Approach to Semantics of Multi-Valued Logic Programs, Tech. Report RT 5006, IBM Tokyo, April 9th, 1990.

[37] D. Perlis. (1985) Languages with Self-Reference I: Foundations , Artificial Intelligence, 25, pp. 301-322.

[38] D. Perlis. (1988) Languages with Self-Reference II: Knowledge,Belief, and Modality, Artificial Intelligence, 34, pp. 179-212.

[39] D. C. Rine. (1986) Some Relationships Between Logic Programming and Multiple-Valued Logic, Proc. IEEE Intl. Symp. on Multiple-Valued Logic, pps 160–163.

[40] E. Shapiro. (1983) Logic Programs with Uncertainties: A Tool for Implementing Expert Systems, Proc. IJCAI ’83, pp. 529–532, William Kauffman.

[41] E. Shortliffe. (1976) Computer-Based Medical Consultation: MYCIN, Elsevier Science.

[42] Y. Shoham. (1988) Reasoning About Change, MIT Press.

[43] V.S. Subrahmanian. (1987) On the Semantics of Quantitative Logic Programs, Proc. 4th IEEE Symposium on Logic Programming, Computer Society Press, Washington DC, pp. 173-182.

[44] V. S. Subrahmanian. (1990) Mechanical Proof Procedures for Many Valued Lattice Based Logic Programming, to appear in: Journal of Non-Classical Logic, 1990.

[45] V. S. Subrahmanian. (1988) Foundations of Metalogic Programming, in: Proc. of the Workshop on Meta-Programming in Logic Programming, (ed. J. Lloyd), Bristol, UK.

[46] V.S. Subrahmanian. (1989) Paraconsistent Disjunctive Deductive Databases, to appear in: Theoretical Computer Science, early 1992.

[47] M.H. van Emden. (1986) Quantitative Deduction and its Fixpoint Theory, Journal of Logic Programming, 4, 1, pp. 37-53.