Uniform Proofs and Disjunctive Logic Programming (Extended Abstract)†

Gopalan Nadathur‡  Donald W. Loveland
Department of Computer Science  Department of Computer Science
University of Chicago  Duke University
1100 E 58th Street, Chicago, IL 60637  Box 90129, Durham, NC 27708-0129

gopalan@cs.uchicago.edu                      dwl@cs.duke.edu

Abstract

One formulation of the concept of logic programming is the notion of Abstract Logic Programming Language, introduced in [8]. Central to that definition is uniform proof, which enforces the requirements of inference direction, including goal-directedness, and the duality of readings, declarative and procedural. We use this technology to investigate Disjunctive Logic Programming (DLP), an extension of traditional logic programming that permits disjunctive program clauses. This extension has been considered by some to be inappropriately identified with logic programming because the indefinite reasoning introduced by disjunction violates the goal-oriented search directionality central to logic programming. We overcome this criticism by showing that the requirement of uniform provability can be realized in a logic more general than that of DLP under a modest, sound, modification of programs. We use this observation to derive inference rules that capture the essential proof structure of InH-Prolog, a known proof procedure for DLP.

1 Introduction

A class of sequent calculus proofs called uniform proofs is identified in [8] and used as a means for determining if a given logical language can serve as a basis for logic programming. The main characteristic of a uniform proof is that it reflects a goal-directedness in proof-search: the objective at any stage in the search is to construct a proof of a single (goal) formula from a collection of assumptions and if this formula is nonatomic, then the search proceeds by first processing its top-level logical symbol. Viewed differently, the logical symbols in the formulas being proved become primitives for directing search and the inference rules pertaining to these symbols become specifications of their search semantics. Classes of formulas and proof relations provide a basis for logic programming just in case provability in their context entails the existence of a uniform proof. The virtue of this “uniform proof property” is that it permits a duality between a declarative and a search-related reading for logical symbols that seems central to a programming use of logic. An auxiliary benefit of the property is that it can be used for describing efficient proof procedures for the underlying logical language [7, 10].

A central characteristic of disjunctive logic programming is that it allows for disjunctive information in the assumption set or program. The ability to express and process indefinite information and case constructions occur in real life and mechanisms to handle such specifications are important. Attention has focused on the semantics of disjunctive logic programming [1, 2, 11], proof procedures [4, 12] and applications to disjunctive databases [9, 13, 14]. One point of view of each of these topics appears in the book [3].

The basic requirement of disjunctive logic programming, that disjunctive information be representable in the assumption set, appears to be at variance with the desire for the uniform proof property to hold. For example, suppose that our assumption set contains the formula p(a) ∨ p(b) and that our goal is to prove ∃x p(x). To obtain a uniform proof of this formula, it is necessary to be able to prove p(t) for some specific term t; this is a natural outcome of goal-directedness and the limitation of a “goal” to a single formula. It is obviously not possible to construct such a proof. Notice, however, that ∃x p(x) is provable from p(a)∨p(b) in most logical systems.

† Work on this paper has been partially supported by NSF grants CCR-92-08465 (Nadathur) and CCR-91-16203 (Loveland) and a grant from the Konrad-Zuse Programm (Nadathur).

‡ On leave till July 1995 at Institut für Informatik, Ludwig-Maximilians Universität, München.

We attempt to reconcile this difference between the presence of disjunctive information and the desire for uniform proofs in this paper. Our approach in doing this is the following. Suppose that we wish to show that a formula G follows from a set of assumption formulas Γ in either classical or intuitionistic logic. We may, in general, not be able to do this by looking only for a uniform proof. However, we show that, if we restrict the syntax of G and the formulas in Γ in such a way that all of disjunctive logic programming is still included, a simple augmentation of Γ makes the search for a uniform proof a complete strategy. In particular, if the necessary syntactic restrictions are satisfied, then a uniform proof exists for G from Γ, G ⊃ ⊥ if and only if there is a classical or an intuitionistic proof for G from Γ. This observation has a practical benefit in that it forms the basis for a proof procedure for our formulas (under a reduction to clausal form) that is a natural generalization of the one usually employed in logic programming. The main new aspect of this procedure is that it has a rule for “backchaining” that is sensitive to the presence of disjunctive information. The restart mechanism of nH-Prolog [4, 5] is used for dealing with this possibility and our procedure is, in fact, an abstract presentation of the InH-Prolog procedure [6].

2 Logical preliminaries

We shall work within the framework of a first-order logic in this paper. The logical symbols that we shall use are ⊤, ⊥, ∧, ∨, ⊃, ∃, and ∀; the first two symbols are intended to denote the tautologous and the contradictory propositions, respectively. The symbol ¬ is excluded from our vocabulary, but it can be defined in terms of the other symbols present: ¬A is a shorthand for (A ⊃ ⊥).

Notions of derivation that are of interest to us are formalized by sequent calculi. A sequent in our context will be a pair of multisets of formulas. The pair will, as usual, be written as Γ ⟶ Δ, assuming that Γ and Δ are its elements. Such a sequent is an axiom if either ⊤ ∈ Δ or for some A that is either ⊥ or an atomic formula, it is the case that A ∈ Γ and A ∈ Δ. The rules that may be used in constructing sequent proofs are those that can be obtained from the schemata shown in Figure 1. In these schemata, Γ, Δ and Θ stand for multisets of formulas, B and D stand for formulas, c stands for a constant, x stands for a variable and t stands for a term. The notation B, Γ (Δ, B) is used here for a multiset containing the formula B whose remaining elements form the multiset Γ (respectively, Δ). Further, expressions of the form [t/x]B are used to denote the result of replacing all free occurrences of x in B by t, with bound variables being renamed as needed to ensure the logical correctness of these replacements. There is the usual proviso with respect to the rules produced from the schemata ∃-L and ∀-R: the constant that replaces c should not appear in the formulas that form the lower sequent. The purpose of the schemata contr-L and contr-R is to blur the distinction between sets and multisets, and so we will be ambivalent about this difference at times. However, this distinction can be important in a situation where these contraction rules are not present.

We will be interested in three notions of derivability for sequents of the form Γ ⟶ B. A C-proof for such a sequent is a derivation obtained by making arbitrary uses of the inference rules. We denote the existence of such a proof, which is a classical proof, for the sequent by writing Γ ⊢_{C} B. I-proofs, that formalize the notion of intuitionistic derivability, are C-proofs in which every sequent has exactly one formula in its succedent. We write Γ ⊢_{I} B to indicate the existence of an I-proof for Γ ⟶ B. Finally, a uniform proof is an I-proof in which any sequent whose succedent contains a nonatomic formula occurs only as the lower sequent of an inference rule that introduces the top-level logical symbol of that formula. Notice that if Γ ⟶ B has a uniform proof, then the following must be true with respect to this proof:

(1) If B is C ∧ D, then the sequent must be inferred by ∧-R from Γ ⟶ C and Γ ⟶ D.

(2) If B is C ∨ D then the sequent must be inferred by ∨-R from either Γ ⟶ C or Γ ⟶ D.

(3) If B is ∃x P then the sequent must be inferred by ∃-R from Γ ⟶ [t/x]P for some term t.

(4) If B is C ⊃ D then the sequent must be inferred by ⊃-R from C, Γ ⟶ D.

(5) If G is ∀x P then, for some constant c that does not occur in the given sequent, it must be the case that the sequent is inferred by ∀-R from Γ ⟶ [c/x]P.

These properties permit the search for a uniform proof to proceed in a goal-directed fashion with the top-level structure of the goal, i.e., the formula being proved, controlling the next step in the search at each stage. We shall write Γ ⊢_{O} B to denote the existence of a uniform proof for Γ ⟶ B. Letting D and G denote collections of formulas and ⊢ denote a chosen proof relation, an abstract logic programming language is defined in [8] as a triple ⟨D, G, ⊢⟩ such that, for all B, B, Γ ⟶ Δ

contr-L

B, Γ ⟶ Δ

Γ ⟶ Δ, B, B

contr-R

Γ ⟶ Δ, B

\begin{matrix}Γ ⟶ Δ, ⊥ \\ ⊥ & -R \\ Γ ⟶ Δ, D \end{matrix}

\begin{aligned}B, D, Γ ⟶ Δ \\ & ∧-L \\ B ∧ D, Γ ⟶ Δ \end{aligned}  \begin{aligned}Γ ⟶ Δ, B & Γ ⟶ Δ, D \\ & ∧-R \\ Γ ⟶ Δ, B ∧ D \end{aligned}
B, Γ ⟶ Δ  D, Γ ⟶ Δ ∨-L B ∨ D, Γ ⟶ Δ

\begin{aligned}Γ ⟶ Δ, B \\ & ∨-R \\ Γ ⟶ Δ, B ∨ D \end{aligned}  \begin{aligned}Γ ⟶ Δ, D \\ & ∨-R \\ Γ ⟶ Δ, B ∨ D \end{aligned}
B ⊃ D, Γ ⟶ B, Δ  D, Γ ⟶ Θ ⊃-L B ⊃ D, Γ ⟶ Δ, Θ \begin{aligned}B, Γ ⟶ Δ, D \\ & ⊃-R \\ Γ ⟶ Δ, B ⊃ D \end{aligned}

\begin{aligned}[t/x]B, Γ ⟶ Δ \\ & ∀-L \\ ∀x B, Γ ⟶ Δ \end{aligned}  \begin{aligned}Γ ⟶ Δ, [t/x]B \\ & ∃-R \\ Γ ⟶ Δ, ∃x B \end{aligned}

\begin{aligned}[c/x]B, Γ ⟶ Δ \\ & ∃-L \\ ∃x B, Γ ⟶ Δ \end{aligned}  \begin{aligned}Γ ⟶ Δ, [c/x]B \\ & ∀-R \\ Γ ⟶ Δ, ∀x B \end{aligned}

Figure 1: Rules for Deriving Sequents

finite subsets P of D and all G ∈ G, P ⊢ G if and only if P ⊢_{O} G.

Our final observation concerns the so-called Cut rule that has the following form:

\frac{Γ_{1} ⟶ B, Δ_{1} B, Γ_{2} ⟶ Δ_{2}}{Γ_{1}, Γ_{2} ⟶ Δ_{1}, Δ_{2}}

It is well-known that this rule is admissible with respect to classical and intuitionistic provability, i.e., the same set of sequents have derivations with and without this rule. We use this fact in the next section.

3 A disjunctive logic programming language

A logic programming language can be described in a proof-theoretic setting by identifying classes of formulas that can serve as program clauses and queries and a proof relation that can be used to derive a query from a given collection of program clauses. Our present interest is that we be able to represent disjunctive information in programs. This leads naturally to the definition of program clauses and queries as the (closed) G- and D-formulas given by the syntax rules

\begin{aligned}G & ::= & A | G ∧ G | G ∨ G | ∃x G \\ D & ::= & A | G ⊃ D | D ∧ D | D ∨ D | ∃x D | ∀x D \end{aligned}

in which A represents an atomic formula distinct from ⊥. The main difference between the formulas presented here and those used to define logic programming based on Horn clauses in [8] is that program clauses (i.e., the D-formulas) are permitted to contain disjunctions and existential quantifications. The traditional description of disjunctive logic programming uses formulas in clausal form. The defining characteristic in this situation is that clauses with “multiple” heads are permitted in programs. It is easily seen that our D-formulas encompass such formulas. In the converse direction, our formulas can, as will become obvious presently, be translated into an equivalent clausal form.

To complete the description of our language, it is necessary to specify the proof relation that is to provide its declarative semantics. The relation that is generally employed for this purpose in disjunctive logic programming is classical provability. In the present context, we have another choice, namely intuitionistic provability. It turns out that it is actually immaterial which of these relations is used since a sequent of the kind we are interested in has a derivation under one if it has a derivation under the other. This observation is of importance in our later analysis relating to uniform provability and so is established below.

Lemma 1 Let Γ be a multiset of formulas and let B_{1}, …, B_{n} be formulas. If Γ ⟶ B_{1}, …, B_{n} has a C-proof in which the rules ⊃-R and ∀-R are not used, then Γ ⟶ B_{1} ∨ … ∨ B_{n} has an I-proof.

Lemma 1 is proved by an induction on the height of a (cut-free) C-proof of Γ ⟶ B_{1}, …, B_{n}. It is easily seen to be true in the base case. For the inductive step, we consider the cases for the last rule. For instance, suppose the last rule is an ∃-R. Then the derivation at the end has the following form:

\frac{Γ ⟶ B_{1}, …, [t/x]B_{i}, …, B_{n}}{Γ ⟶ B_{1}, …, ∃x B_{i}, …, B_{n}}.

By hypothesis, Γ ⟶ B_{1} ∨ … ∨ [t/x]B_{i} ∨ … ∨ B_{n} has an I-proof. Now, it is easily seen that

B_{1} ∨ … ∨ [t/x]B_{i} ∨ … ∨ B_{n} ⟶ B_{1} ∨ … ∨ ∃x B_{i} ∨ … ∨ B_{n}

has an I-proof. The desired conclusion follows from these observations by the admissibility of the Cut rule. The other cases have similar arguments.

Theorem 2 Let Γ be a multiset of D-formulas and let G be a G-formula. Then Γ ⟶ G has a C-proof if and only if it has an I-proof.

Proof. The if direction is obvious. For the only if direction, we observe that there can be no occurrences of ∀-R and ⊃-R in a cut-free C-proof of Γ ⟶ G. The desired conclusion now follows by virtue of Lemma 1.

□

The truth of Lemma 1 is independent of the appearance of the ⊥-R rule in C-proofs and so Theorem 2 remains true even if our G- and D-formulas are extended by letting A in the syntax rules defining them be ⊥ in addition to atomic formulas. Incorporating this extension permits D-formulas to also encode negative clauses: the clause (¬B_{1} ∨ … ∨ ¬B_{m}) can be written equivalently as (B_{1} ∧ … ∧ B_{m}) ⊃ ⊥. Now, the (classical) unsatisfiability of a set of clauses Γ is equivalent to the existence of a C-proof for Γ ⟶ ⊥. Thus, Theorem 2 shows that the reducibility of an arbitrary formula to clausal form provides another encoding of classical logic in intuitionistic logic.

4 Uniform provability

The language described in the previous section does not have the uniform proof property. For instance, consider the sequent

p(a) ∨ p(b) ⟶ ∃x p(x).

This sequent has both a C-proof and an I-proof but it does not have a uniform proof. Notice that p(a) ∨ p(b) is a program clause of our language and ∃x p(x) is a query.

Although the uniform proof property does not hold directly of our language, it holds of it in a derivative sense. In particular, suppose that Γ is a (multi)set of program clauses and that G is a query. Then Γ ⟶ G has a C- or an I-proof if and only if G ⊃ ⊥, Γ ⟶ G has a uniform proof. This surprising observation has an interesting consequence: it can be used to describe a proof procedure for our language that is goal-directed and that differs from the procedure usually employed with Horn clauses only in the structure of the backchaining rule. We explore this aspect of our observation in the next section. The rest of this section is devoted to showing that the observation is, in fact, true.

We first note that the mentioned transformation of the assumption set is sound and complete with respect to intuitionistic logic.

Lemma 3 Let Γ be a multiset of program clauses and let G be a query. Then G ⊃ ⊥, Γ ⊢_{I} G if and only if Γ ⊢_{I} G.

Proof. The if direction is obvious. For the only if direction, we observe first that if G ⊃ ⊥, Γ ⊢_{I} G then G ⊃ ⊥, Γ ⊢_{C} G and, hence, (G ⊃ ⊥) ∨ G, Γ ⊢_{C} G. Noting that ⊢_{C} (G ⊃ ⊥)∨G and using the Cut rule, we see that Γ ⊢_{C} G. The desired observation now follows from Theorem 2.

□

Theorem 4 Let Γ be a multiset of program clauses and let G be a query. Then G ⊃ ⊥, Γ ⊢_{I} G if and only if G ⊃ ⊥, Γ ⊢_{O} G.

Proof. The if direction is immediate. We provide only a sketch of the argument for the only if direction.

Suppose that G ⊃ ⊥, Γ ⟶ G has a cut-free Iproof. Then it must have one in which (a) for every non-atomic formula appearing in the right of a sequent there is a rule introducing its top-level symbol and (b) no left rule immediately succeeds a right rule pertaining to a top-level logical symbol of a formula in a common sequent except in the following cases: the left rule is ∨-L and the right rule is either ∃-L or ∨-R or the left rule is ∃-L and the right rule is ∃-R. (To ensure (a) it may be necessary to introduce some inference steps right after ⊥-R rules and (b) follows from known permutabilities for intuitionistic calculus applied to the kinds of sequents that arise in our situation.) Let us call a I-proof satisfying the requirements mentioned above an I′-proof. Now, let R be either an ∨-L or an ∃-L rule. We associate a measure with R that is the count of the number of connectives and quantifiers that appear in the succedent of the lower sequent of R. We use this measure to associate one with an I′-proof Ξ as follows: the measure of Ξ is the sum of the measures of all the ∨-L and ∃-L rules that appear in Ξ. We claim that any I′-proof of G ⊃ ⊥, Γ ⟶ G that has a nonzero such measure can be transformed into an I′-proof of smaller measure. It follows easily from this that G ⊃ ⊥, Γ ⟶ G has a uniform proof.

To show the claim we consider the various cases by which an I′-proof of G ⊃ ⊥, Γ ⟶ G might have nonzero measure. One possibility is that there is an ∨-L rule right after an ∨-R. For instance, the following steps might appear somewhere in the derivation:

\begin{aligned}B, Γ′ ⟶ D \\ & ∨-R \\ B, Γ′ ⟶ D ∨ E \end{aligned} C, Γ′ ⟶ D ∨ E ∨-L B ∨ C, Γ′ ⟶ D ∨ E

We shall assume that D and E are atomic — this assumption can be dispensed with in a detailed proof. Our objective in this case is to show that the use of ∨-L and ∨-R rules above can be reordered, thereby reducing the overall measure.

Using the fact that what is displayed above is a subpart of an I′-proof of G ⊃ ⊥, Γ ⟶ G, it can be shown that C, Γ′ ⟶ G has an I′-proof of smaller measure than the one for G ⊃ ⊥, Γ ⟶ G — the essential idea is to mimic the I′-proof for G ⊃ ⊥, Γ ⟶ G and to note that at least one use of the ∨-L rule — the one shown above — is not needed. By induction it follows then that C, Γ′ ⟶ G has an I′-proof of zero measure. It can also be seen that C, Γ′ can be written as either G ⊃ ⊥, Γ′′ or ⊥, Γ′′. We assume the former; the argument is simpler if the latter is true. Thus, we can construct the following sub-derivation:

B, Γ′ ⟶ D \begin{matrix}C, Γ′ ⟶ G & \begin{matrix}⊥, Γ′′ ⟶ ⊥ \\ ⊥ & -R \\ ⊥, Γ′′ ⟶ D \end{matrix} \\ ⊃-L \\ C, Γ′ ⟶ D \end{matrix} ∨-L B ∨ C, Γ′ ⟶ D ∨-R B ∨ C, Γ′ ⟶ D ∨ E

Using the known I′-proofs of B, Γ′ ⟶ D and C, Γ′ ⟶ G together with this to replace the earlier subderivation,we obtain the desired I′-proof of reduced measure.

The other cases are amenable to a similar argument.

□

There is a constructive content to the discussions in this section that we attempt to bring out by means of an example. Consider the following I-proof of p(a) ∨ p(b) ⟶ ∃x p(x):

\begin{aligned}p(a) ⟶ p(a) \\ & ∃-R \\ p(a) ⟶ ∃x p(x) \end{aligned}  \begin{aligned}p(b) ⟶ p(b) \\ & ∃-R \\ p(b) ⟶ ∃x p(x) \end{aligned} ∨-L p(a) ∨ p(b) ⟶ ∃x p(x)

By following the argument in the proof of Theorem 4, we obtain from this I-proof the uniform proof for ∃x p(x) ⊃ ⊥, p(a) ∨ p(b) ⟶ ∃x p(x) that is shown in Figure 2.

5 A deductive calculus with directionality

A virtue of the uniform proof property is that it provides some control over the proof search process: So long as the formula in the succedent of the sequent is non-atomic, the top-level connective can be used to direct the next step in the search. However, the way to proceed is not as clear in the situation when the succedent is an atomic formula since a variety of left rules may be possible. An analogous problem arises in the case of Horn clauses. The solution in that situation is to reduce the left rules to a single backchaining rule; of course, some nondeterminism persists in that a choice has to be made of the program clause that is to be backchained over. The surprising observation is that there is a natural generalization of this backchaining rule that can be used to similar effect even in the context of our language. We show this to be the case in this section.

To permit the statement of this backchaining rule, it is necessary, first of all, to consider a simplification to the syntax of program clauses. In particular, we assume henceforth that these are closed D-formulas given by the syntax rule

D ::= A ∨ … ∨ A | G ⊃ (A ∨ … ∨ A) | ∀x D;

as before, A is intended to be a syntactic variable for an atomic formula distinct from ⊥ in this rule. A program clause in the syntax of Section 3 can be transformed into a classically equivalent set of program clauses in the current syntax. By invoking Theorem 2, we see that this transformation is also intuitionistically acceptable. Notice that Theorem 2 is used in an essential way in justifying this step since operations like (static) Skolemization and the raising of scope of universal quantifiers that are used in the transformation process are, in general, not intuitionistically valid. As a specific example, ∀x (D_{1}(x) ∨ D_{2}) is not necessarily intuitionistically equivalent to (∀x D_{1}(x)) ∨ D_{2} even if x has no free occurrences in D_{2}.

p(a), ∃x p(x) ⊃ ⊥ ⟶ p(a)  \begin{matrix}\begin{aligned}p(b), ∃x p(x) ⊃ ⊥ ⟶ p(b) \\ & ∃-R \\ p(b), ∃x p(x) ⊃ ⊥ ⟶ ∃x p(x) \end{aligned} & \begin{matrix}⊥, p(b) ⟶ ⊥ \\ ⊥ & -R \\ ⊥, p(b) ⟶ p(a) \end{matrix} \\ ⊃-L \\ p(b), ∃x p(x) ⊃ ⊥ ⟶ p(a) \end{matrix} ∨-L p(a) ∨ p(b), ∃x p(x) ⊃ ⊥ ⟶ p(a) ∃-R ∃x p(x) ⊃ ⊥, p(a) ∨ p(b) ⟶ ∃x p(x)

Figure 2: A Uniform Proof for ∃x p(x) ⊃ ⊥, p(a) ∨ p(b) ⟶ ∃x p(x)

If the syntax of our program clauses is simplified in this manner, then the rules ∃-L and ∧-L can be excluded from our calculus since they cannot occur in cut-free proofs of sequents of the kind we are interested in. The contr-L rule can also be eliminated if we restate the ∀-L rule as follows:

\frac{[t/x]B, ∀x B, Γ ⟶ Δ}{∀x B, Γ ⟶ Δ}

(We are effectively building contraction into this rule.) We hereafter assume this modification to the ∀-L rule.

Let Γ be a set of program clauses and let G be a query. By virtue of Theorem 4, a sound and complete strategy for finding a C- or an I-proof for Γ ⟶ G is to look for a uniform proof for G ⊃ ⊥, Γ ⟶ G. An analysis of the proof of the theorem indicates that the enhancement to the assumption set is unnecessary if we change the ∨-L rule to be the following:

\frac{B, Γ ⟶ A D, Γ ⟶ G}{B ∨ D, Γ ⟶ A}

In this rule, A stands for an atomic formula and G for the original query. Notice that this is a rule that is dependent on the original query and we indicate this dependence by using the name ∨-L_{G} for it. The discussions that follow must also be understood relative to this choice of G.

By incorporating the various modifications described above, we obtain a calculus in which the only left rules are ∨-L_{G}, ⊃-L and ∀-L. Further, assuming that Γ is a (multi)set of program clauses, the classical and intuitionistic provability of Γ ⟶ G is equivalent to the uniform provability of the same sequent in this modified calculus. The backchaining rule that is of interest to us combines the three left rules of our modified calculus into a single rule.

Definition 1. Let D be a program clause. Then [D] denotes a collection of pairs of sets of formulas given as follows:

(1) If D is A_{1} ∨ … ∨ A_{n}, then

[D] = {⟨∅, {A_{1}, … A_{n}}⟩}.

(2) If D is G ⊃ (A_{1} ∨ … ∨ A_{n}), then

[D] = {⟨{G}, {A_{1}, …, A_{n}}⟩}.

(3) If D is ∀x D_{1}, then

[D] = ⋃{[[t/x]D_{1}] | t is a term}.

This notation is extended to a (multi)set Γ of program clauses as follows: [Γ] = ⋃{[D] | D ∈ Γ}.

Definition 2. Let Γ be a (multi)set of program clauses. As mentioned already, G is assumed to be a fixed query.

(1) The ATOMIC rule is the following

\frac{A_{1}, Γ ⟶ G  …  A_{n}, Γ ⟶ G}{Γ ⟶ C}

provided that ⟨∅, {C, A_{1}, …, A_{n}}⟩ ∈ [Γ]. In the degenerate case, i.e., when the second component of the pair shown is simply {C}, this rule has no upper sequents.

(2) The BACKCHAIN rule is the following

\frac{Γ ⟶ G′ A_{1}, Γ ⟶ G … A_{n}, Γ ⟶ G}{Γ ⟶ C}

provided that ⟨{G′}, {C, A_{1}, …, A_{n}}⟩ ∈ [Γ]. In the degenerate case, i.e., when the second component of the pair shown is simply {C}, this rule has Γ ⟶ G′ as its only upper sequent.

The rules defined above are obvious generalizations of the ones that make use of program clauses in the usual Horn clause setting. The latter rules correspond, in fact, to the degenerate versions of our rules. From a proof search perspective, both the ATOMIC and the BACKCHAIN rules exhibit directionality: the atomic formula to be proved determines the clauses whose use is to be considered.

Lemma 5 Let Γ be a multiset of program clauses and let C be an atomic formula. Then Γ ⟶ C has a uniform proof with l sequents in the calculus with the original right rules and the left rules ∨-L_{G}, ⊃-L and ∀-L, if and only if one of the following conditions hold:

(1) For some A_{1}, …, A_{n}, ⟨∅, {C, A_{1}, …, A_{n}}⟩ ∈ [Γ] and, for 1 ≤ i ≤ n, A_{i}, Γ ⟶ G has a uniform proof with fewer than l sequents in the same calculus.

(2) For some A_{1}, …, A_{n}, ⟨{G′}, {C, A_{1}, …, A_{n}}⟩ ∈ [Γ] and Γ ⟶ G′ and, for 1 ≤ i ≤ n, A_{i}, Γ ⟶ G have uniform proofs with fewer than l sequents in the same calculus.

Proof. By an induction on the size of the uniform proof for Γ ⟶ C.

□

Theorem 6 Let Γ be a set of program clauses and let G be a query. Then Γ ⟶ G has a C-proof or an Iproof if and only if it has a uniform proof in a calculus containing all the right rules and the ATOMIC and BACKCHAIN rule relativized to G.

Proof. Recall that a sequent of the kind we are interested in has a C-proof or an I-proof just in case it has a uniform proof in a calculus containing all the right rules, ∨-L_{G}, ⊃-Land ∀-L. The theorem follows by an easy induction from this and Lemma 5.

□

The final calculus described in this section can translate into a proof procedure very close to one already in the literature in the Disjunctive Logic Programming field, namely, the Inheritance Near-Horn Prolog procedure (InH-Prolog)[6, 12]. The ATOMIC and BACKCHAIN rules implement precisely the restart rule of InH-Prolog, and with the superimposed search ordering of InH-Prolog providing an ordering of pursuit of the upper sequents of these rules, the mapping from proof searches in this calculus to InH-Prolog proof search is nearly one-to-one. This relationship will be made explicit in the full paper. Finally, a very similar calculus can also be described in the situation where the atomic formula in the syntax rules for program clauses and queries is permitted to be ⊥. Indeed, this is the usual presentation format for InH-Prolog, although it is known that use of the original goal is interchangeable with use of ⊥ for all procedures in the Near-Horn Prolog family. Again, this will be addressed in the full version of this paper.

6 Conclusion

In this paper, we have investigated a generalization of the logical language underlying disjunctive logic programming from a proof-theoretic perspective. While the uniform proof property described in [8] does not hold of this language, we have shown that a modest addition to programs makes the search for a uniform proof a complete strategy. This observation has been utilized to describe a deductive calculus that captures the essence of the proof structure of Inheritance near-Horn Prolog, one of the proof procedures earlier proposed for disjunctive logic programming. This methodology also provides a basis for analyzing other proposed proof procedures. A fuller discussion of these issues will appear in a complete version of the paper.

References

[1] A. Van Gelder, K.A. Ross, and J.S. Schlipf. The well-founded semantics for general logic programs. J. ACM, 38(3):620–650, 1991.

[2] J. Lobo, J. Minker, and A. Rajasekar. Extending the semantics of logic programs to disjunctive logic programs. In G. Levi and M. Martelli, editors, Logic Programming: Proc. of the Sixth Int’l Conf., Lisbon, Portugal, 1989.

[3] J. Lobo, J. Minker, and A. Rajasekar. Foundations of Disjunctive Logic Programming. MIT Press, Cambridge, MA, 1992.

[4] D.W. Loveland. Near-Horn Prolog. In J. Lassez, editor, Logic Programming: Proc. of the Fourth Int’l Conf., pages 456–469. MIT Press, 1987.

[5] D.W. Loveland. Near-Horn Prolog and beyond. J. Automated Reasoning, 7:1–26, 1991.

[6] D.W. Loveland and D.W. Reed. A near-Horn Prolog for compilation. In J. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT Press, 1991.

[7] Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497–536, 1991.

[8] Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991.

[9] J. Minker. On indefinite databases and the closed world assumption. In Lecture Notes in Computer Science 138, pages 292–308. Springer-Verlag, Berlin, 1982.

[10] Gopalan Nadathur. A proof procedure for the logic of hereditary Harrop formulas. Journal of Automated Reasoning, 11(1):115–145, August 1993.

[11] T.C. Pryzmusinski. Stationary semantics for disjunctive logic programs and deductive databases. In S. Debray and M. Hermenegildo, editors, Logic Programming: Proc. of the 1990 North American Conf., pages 40–62. MIT Press, 1990.

[12] D.W. Reed, D.W. Loveland, and B.T. Smith. An alternative characterization of disjunctive logic programs. In V. Saraswat and K. Ueda, editors, Logic Programming: Proc. of the 1991 Int’l Symp. MIT Press, 1991.

[13] K.A. Ross and R.W. Topor. Inferring negative information from disjunctive databases. J. Automated Reasoning, 4(2):397–424, 1988.

[14] A. Yahya and L.J. Henschen. Deduction in non-Horn databases. J. Automated Reasoning, 1(2):141–160, 1985.