A Logical Analysis of Modules in Logic Programming

Dale Miller Computer and Information Science University of Pennsylvania Philadelphia, PA 19104

Running Title: A Logical Analysis of Modules

Abstract: We present a logical language which extends the syntax of positive Horn clauses by permitting implications in goals and in the bodies of clauses. The operational meaning of a goal which is an implication is given by the deduction theorem: a goal D ⊃ G is provable from a program P if the goal G is provable from the larger program P ∪ {D}. This paper explores the qualitative nature of this extension to logic programming. For example, if the formula D is the conjunction of universally quantified clauses, we interpret the goal D ⊃ G as a request to load the code in D prior to attempting G and then unload that code after G succeeds or fails. This extended use of implication provides a logical explanation of parametric modules, some uses of Prolog’s assert predicate, and aspects of abstract datatypes. Both a model theory and proof theory are presented for this logical language. In particular, we show how to build a Kripke-like model for programs by a fixed point construction and show that the operational meaning of implication mentioned above is sound and complete for intuitionistic logic. We also examine a weak notion of negation which is easily implemented in this language and show how database constraints can be represented by it.

This work has been supported by ARO grant DAAG-29-84-K-0061 and DARPA grant N000-14-85-K-0018.

A Logical Analysis of Modules 1. Implications as Goals

1. Implications as Goals We shall assume that our logical language is a first-order language with denumerably

many constants, variables, functions symbols, and predicates (at all arities). This language will contain the following logical constants as primitives: ∧ (conjunction), ∨ (disjunction), and ⊃ (implication) are binary connectives, ∀ (for all) and ∃ (exists) are quantifiers, and ⊥ (falsehood) is a 0-ary logical constant. When we have the occasion to write negation, ∼B, we will assume that it defined as B ⊃ ⊥. This convention will be explained in Section 7 when negation is first considered. ⊥ is not an atomic formula.

Let A be a syntactic variable which ranges over atomic formulas. Let G range over a class of formulas, called goal formulas, to be specified shortly. We shall assume, however, that all atomic formulas are also goal formulas. Definite clauses, denoted by the syntactic variable D, are defined recursively as:

D := A | G ⊃ A | ∀x D | D_{1} ∧ D_{2}.

Definite clauses, as well as atomic and goal formulas, may contain free variables. P will be a syntactic variable for sets of definite clauses. Such a set will often be called a program. We shall always assume that a program is a finite set.

Let P be a set of definite clauses. Define [P] to be the smallest set of formulas satisfying the following recursive conditions:

∘ P ⊆ [P].

∘ If D_{1} ∧ D_{2} ∈ [P] then D_{1} ∈ [P] and D_{2} ∈ [P].

∘ If ∀x D ∈ [P] then [x/t]D ∈ [P] for all terms t. Here [x/t]D denotes the result of substituting t for free occurrences of x in D.

In the case that G is a goal formula and P a set of definite clauses, we shall use the expression P ⊢_{O} G to mean that G can be derived from P, or that G is an output of P. We use the subscript O here to indicate that we are thinking about an operational definition of derivation, i.e., one that captures an intuitive sense of computation. No a priori relation between ⊢_{O} and other logical senses of derivation or validity are assumed.

We present six proof rules for ⊢_{O} below. The first two are related to the structure of definite clauses.

(1) P ⊢_{O} A if A ∈ [P], and

(2) P ⊢_{O} A if there is a formula (G ⊃ A) ∈ [P] and P ⊢_{O} G. These two proof rules provide the basic elements needed to define recursive procedures. A clause of the form ∀x̄(G ⊃ A) (where ∀x̄ represents a list of universally quantified variables) is treated as a specification of how a procedure, the name of which is the head of A, can nondeterministically call other code, i.e., the formula G.

To complete the description of a logic programming language, we need to describe the class of goal formulas and how non-atomic goals can be operationally proved from a program. We can define a logic equivalent to positive Horn clauses by letting goal formulas be defined as

G := A | G_{1} ∧ G_{2} | G_{1} ∨ G_{2} | ∃xG

and adding the following proof rules:

(3) P ⊢_{O} G_{1} ∨ G_{2} if P ⊢_{O} G_{1} or P ⊢_{O} G_{2}.

(4) P ⊢_{O} G_{1} ∧ G_{2} if P ⊢_{O} G_{1} and P ⊢_{O} G_{2}.

(5) P ⊢_{O} ∃xG if there is some term t such that P ⊢_{O} [x/t]G. In this context, the logical connectives ∧ and ∨ provide for the specification of nondeterministic and and or branches in the search for a derivation. The quantifier ∃ specifies an infinite non-deterministic or branch where the disjuncts are parameterized by the set of terms.

A program in this logic programming language is equivalent to a conjunction of positive Horn clauses. For example, the definite clause

∀z∀y [(∃x R(x, y) ∧ P (y, z)) ∨ R(z, z) ⊃ P (z, y)]

is operationally equivalent to the definite clause

\begin{matrix}∀z∀y∀x [R(x, y) ∧ P (y, z) ⊃ P (z, y)] ∧ \\ ∀z∀y [R(z, z) ⊃ P (z, y)]. \end{matrix}

Since this normal form exists for this version of definite clauses, the literature concerning the theoretical nature of positive Horn clauses generally does not present the syntax of this logic in this more general setting. In Section 8 we generalize this normal form result for programs.

In the rest of this paper, however, we shall assume that goal formulas have the following more slightly complex syntax

G := A | G_{1} ∧ G_{2} | G_{1} ∨ G_{2} | ∃xG | D ⊃ G,

and that there is the additional proof rule

(6) P ⊢_{O} D ⊃ G if P ∪ {D} ⊢_{O} G. The classes of goal formulas and definite clauses are now defined by mutual recursion.

The “proof rules” above are merely desired properties for the proof predicate ⊢_{O}. We now formalize the meaning of ⊢_{O} by presenting a sequent-style proof system (see [9] and [18]). A sequent is a pair, Γ ⟶ Θ, where both the antecedent Γ and the succedent Θ are possibly empty sets of formulas. When a particular sequent is being displayed, we often simply enumerate the elements of succedents and antecedents without including set brackets. Furthermore, we will often write Γ, B and B, Γ to denote Γ ∪ {B}.

Each of the proof rules (2) — (6) can be written as inference figures in the following manner:

P ⟶ G ; (2) ; P ⟶ A  \begin{aligned}P ⟶ G_{i} \\ & (3) \\ P ⟶ G_{1} ∨ G_{2} \end{aligned}

\begin{aligned}P ⟶ G_{1} & P ⟶ G_{2} \\ & (4) \\ P ⟶ G_{1} ∧ G_{2} \end{aligned}  P ⟶ [x/t]G ; (5) ; P ⟶ ∃x G

P, D ⟶ G (6).

P ⟶ D ⊃ G

Here, of course, G ⊃ A ∈ [P], i = 1 or i = 2, and t is some term. In such inference figures, the sequent(s) appearing above the horizonal line are the upper sequent(s), while the sequent appearing below the line is the lower sequent.

An O-proof for P ⟶ G is a tree whose nodes are labeled with sequents such that (i) the root node is labeled with P ⟶ G, (ii) the internal nodes are instances of one of the above inference figures, and (iii) the leaf nodes are labeled with sequents representing proof rule (1), i.e., with sequents of the form P ⟶ A where A ∈ [P]. Such sequents are called initial sequents.

We shall picture proofs as growing up from their root node. The height of a proof is the length of the longest path from the root to some leaf. The size of a proof is the number of nodes in it.

Inference figures shall refer only to the syntactic objects used to build proofs while proof rules shall refer to properties of the proof predicate ⊢_{O}. The formal meaning of ⊢_{O} can now be given as: P ⊢_{O} G if there is an O-proof for P ⟶ G. The six proof rules given above are now obvious conclusions. Our interests throughout most of this paper will concern operational provability in its nondeterministic sense. That is, it will not matter if there are several such O-proofs or if a depth-first theorem prover could never find such a proof.

Let P_{1} := {q(a), p(b) ⊃ r(b, a), ∀x∀y [r(x, y) ∧ q(y) ⊃ q(f(x))]}. The following is an O-proof of the goal ∃x [p(x) ⊃ q(f(x))] from P_{1}.

\begin{aligned}P_{1}, p(b) ⟶ p(b) \\ & (2) \\ P_{1}, p(b) ⟶ r(b, a) \end{aligned} P_{1}, p(b) ⟶ q(a) (4)

P_{1}, p(b) ⟶ r(b, a) ∧ q(a) (2)

P_{1}, p(b) ⟶ q(f(b)) (6)

P_{1} ⟶ [p(b) ⊃ q(f(b))] (5)

P_{1} ⟶ ∃x [p(x) ⊃ q(f(x))] The size of this proof is 7 and its height is 6.

Although the operational notion of O-proof is intuitive enough, it is natural to ask whether it is, in some sense, logical. Thus consider the following example. Let P_{2} := {p(a) ∧ p(b) ⊃ q}. Is there an O-proof of ∃x (p(x) ⊃ q) from P_{2}? Consider the following tree of sequents.

P_{2}, p(a) ⟶ p(a)  P_{2}, p(a) ⟶ p(b) (4)

P_{2}, p(a) ⟶ p(a) ∧ p(b) (2)

P_{2}, p(a) ⟶ q (6)

P_{2} ⟶ p(a) ⊃ q (5)

P_{2} ⟶ ∃x (p(x) ⊃ q)

This is not a proof because P_{2}, p(a) ⟶ p(b) is not an initial sequent. Regardless of the term used to instantiate the quantifier ∃x in the root sequent, this tree cannot be extended to an O-proof. While it seems reasonable enough that there is no such proof, it is important to notice that the formula

(p(a) ∧ p(b) ⊃ q) ⊃ ∃x (p(x) ⊃ q)

is classically provable. (A classical proof of this formula will be presented in Section 6.) Thus classical logic is not sound with respect to the our operational semantics. The actual logical status of ⊢_{O} will be addressed more fully in Section 6. Until then, we shall simply be concerned with how ⊢_{O} can be used to interpret programs.

In this paper we will not discuss the specifics of how one might actually implement definite clauses into a Prolog-like language which incorporates such implementation mechanisms as backtracking, logical variables, and unification. It is useful, however, to point out two aspects of how such an implementation would need to differ from a more traditional Prolog interpreter. First, explicit quantifiers need to be used in specifying programs. In Prolog, quantifiers in Horn clauses are dropped since free variables in them can be thought of as being universally quantified. Similarly, free variables in goals can be thought of as being existentially quantified. This is not true, however, of definite clauses. For example, only the second of the two goal formulas ∃x(∀y p(x, y) ⊃ q) and (∀x∀y p(x, y) ⊃ q) may be derived from the definite clause p(a, c) ∧ p(b, c) ⊃ q. If explicit quantifiers were dropped, there would be no way to differentiate correctly between these two goals.

If unification and logical variables are used in the standard way to delay and determine substitutions, then a second difference with traditional Prolog systems is forced, namely, that program clauses as well as goals can contain logical variables. For example, consider a goal of the form ∃x (D(x) ⊃ G(x)), i.e., an existentially quantified implication in which the quantified variable can be free on both sides of the implication. If this quantifier is A Logical Analysis of Modules 2. Storing Successful Goals

replaced with a logical (free) variable, say X, then the code D(X) must be added to the current program clauses before attempting to prove G(X). When unification provides substitutions for X, both program clauses and goals must be updated accordingly.

2. Storing Successful Goals Before we examine how our extended use of implication can be used to implement

modules, we first show how implications can be used to provide a scoped and temporary assert mechanism. We illustrate this mechanism by considering how to implement a form of memoization.

Notice that if A is atomic, P ⊢_{O} A ∧ G if and only if P ⊢_{O} A ∧ [A ⊃ G]. The proof of this statement in the forward direction is trivial. The proof of the converse is slightly more difficult and is given below. It should be quite clear that the size of an O-proof of the second formula can at times be much smaller than for the first formula. With the second formula, A does not need to be reproved each time it is needed in the proof of G.

Consider the following Prolog program for computing Fibonacci numbers. In general, we shall use the syntax of [20] to represent example programs.

fib(0,0).
fib(1,1).
fib(N,F) :- N1 is N-1, N2 is N-2, fib(N1,F1),
           fib(N2,F2), F is F1+F2.

For this example, if n is the integer value of the arithmetic expression t then the sequent Γ ⟶ n is t, for any set Γ, will be permitted as an initial sequent. If f_{n} denotes the n^{th} Fibonacci number then the size of the only O-proof of the goal fib(n, f_{n}) is exponential in n.

Consider, however, the following program which employs implicational goals to store previously computed Fibonacci numbers. Here, we have introduced the symbol => to represent implication (:- is the converse of =>).

fib(N,M) :- memo(0,0) => memo(1,1) => fiba(N,M,2).
fiba(N,M,I) :- memo(N,M).
fiba(N,M,I) :- N1 is I-1, N2 is I-2, memo(N1,F1),
              memo(N2,F2), F is F1+F2, I1 is I+1,
              memo(I,F) => fiba(N,M,I1).

In this last program, there exists only one proof of fib(n, f_{n}) and that proof has a size proportional to n.

We now return to the formal justification of this approach to memoization.

A Logical Analysis of Modules 3. Implementing Modules

Theorem 1. If A is atomic, Γ ⊢_{O} A ∧ G if and only if Γ ⊢_{O} A ∧ [A ⊃ G]. Proof. This is trivial in the forward direction. For the proof in the reverse direction, assume that Γ ⊢_{O} A ∧ [A ⊃ G]. Thus Γ ⊢_{O} A and Γ, A ⊢_{O} G. Let T_{1} and T_{2} be Oproofs for Γ ⟶ A and Γ, A ⟶ G, respectively. We need to construct an O-proof for Γ ⟶ G. If A ∈ Γ then Γ = Γ ∪ {A} ⊢_{O} G, so T_{2} is an O-proof for Γ ⟶ G. Assume that A ∉ Γ. Build a tree, T_{3}, by removing A from all the antecedents of sequents in T_{2}. This tree may not be a proof for Γ ⟶ G because there may have been initial sequents of the form Γ′, A ⟶ A in T_{2} which are now of the form Γ′ ⟶ A. These, of course, may no longer be initial sequents. Since Γ ⊆ Γ′, adding the definite clauses Γ′ − Γ to all the antecedents of sequents in the proof T_{1}, we can get an O-proof for Γ′ ⟶ A. Thus, if we add to the top of all such non-initial leaves of T_{3} the appropriate augmented version of T_{1}, we will have an O-proof of Γ ⟶ G. Hence, Γ ⊢_{O} A ∧ G.

After we prove the equivalence of ⊢_{O} to intuitutionistic logic in Section 6, this theorem is easily proven by just noting that A ∧ G is intuitutionistically equivalent to A ∧ (A ⊃ G).

The set of formulas which can be memoized in this fashion is slightly larger than the set of atomic formulas. Such a formula must have the structure of a definite clause and of a goal formula. Let M be a syntactic variable which ranges over the set of formulas described by

M := A | M ⊃ A | M_{1} ∧ M_{2}.

It is easy to show that a formula is a definite clause and a goal formula if and only if it belongs to the class of formulas satisfying this recursive definition. Notice, for example, that all propositional, positive Horn clauses are such formulas.

3. Implementing Modules Consider now how we might reimplement Prolog’s consult predicate with implica-

tional goals. Let classify, scanner, and misc be the names of files containing Prolog code. When these names appear within formulas, assume that they refer to the conjunction of universally quantified definite clauses contained in those files. Now consider the following goal.

               ⊢_{O} misc ⊃ ((classify ⊃ G_{1}) ∧ (scanner ⊃ G_{2}) ∧ G_{3})

This goal will cause each of the three goals G_{1}, G_{2}, and G_{3} to be attempted with different programs. In particular, this single goal will cause the following goals to be attempted:

                            misc, classify ⊢_{O} G_{1}
                             misc, scanner ⊢_{O} G_{2}

misc ⊢_{O} G_{3}.

Implicational goals can, therefore, be used to structure the runtime environment of a program. For example, the code present in classify is essentially hidden during the evaluation of goal G_{2}. This is, of course, very desirable if it had been the case that classify and scanner were written by different people. This mechanism ensures that there will be no conflict between the predicates in these two programs. Current implementations of logic programs generally require that all code be loaded into one area before it can be used. Such a lack of modularity is certainly a weakness of such implementations.

The previous discussion suggests that it would be possible to design a notion of modules for logic programming which is based entirely on the logical meaning of implications. To this end, we will introduce modules as named collections of clauses. For example, the following is a module containing some list manipulation programs.

module lists.
append([],X,X).
append([U|L],X,[U|M]) :- append(L,X,M).
member(X,[X|L]) :- !.
member(X,[Y|L]) :- member(X,L).
memb(X,[X|L]).
memb(X,[Y|L]) :- memb(X,L).

The theory of definite clauses we are considering in this paper does not encompass the cut ! operation. We shall assume, however, that in our examples it will play the same role in controlling backtracking as it does in Prolog.

According to our definitions, a goal could be of the form ∃x [D(x) ⊃ G(x)], where the variable x is free in either or both D(x) and G(x). This suggests that the definite clauses defining a module can contain free variables. Thus a kind of parametric module is possible. Consider the following parametric module:

module sort(Order).
bsort(L1,L2) :-
       append(Sorted,[Big,Small|Rest],L1),
       Order(Small,Big), !,
       append(Sorted,[Small,Big|Rest],BetterL1),
       bsort(BetterL1,L2).
bsort(L1,L1).

This example, as well as others presented later, is technically not first-order because we have a variable which is acting as a predicate. This could be alternatively implemented using such extra-logical tricks as replacing the atom Order(Small,Big) with the two goals G =.. [Order,Small,Big], call(G). There is also a more direct and logical way to provide Prolog with predicate variables by placing it in a higher-order logic [14, 15]. Either approach could be used to give a meaning to this module.

Consider using the sort module to sort the list [2,3,1] in ascending order. Since bsort uses the append predicate, the lists module must be used along with the sort module. The answer substitution for x in the following goal would provide the desired sorted list.

⊢_{O} lists ∧ sort(<) ⊃ ∃x bsort([2, 3, 1], x)

It is unfortunate that in order to use the sort module it was necessary to explicitly reference the lists module, which sort needed to execute successfully. It should be possible for the author of the sort module to import those modules which are needed in the sort module. Implications can again be used to provide this importing mechanism. For example, we could rewrite the sort module as:

module sort(Order).
bsort(L1,L2) :-
   (lists =>
      (append(Sorted,[Big,Small|Rest],L1),
       Order(Small,Big), !,
       append(Sorted,[Small,Big|Rest],BetterL1),
       bsort(BetterL1,L2)
    )).
bsort(L1,L1).

Now we would be able to sort our list with the simple goal

⊢_{O} sort(<) ⊃ ∃x bsort([2, 3, 1], x)

When the body of bsort is attempted as a goal, it will come with the module lists as a hypothesis. Notice that the scope of the lists module in the first bsort clause is over the entire body of that clause. Clearly, its scope could be restricted to just cover the two append goals. This is desirable especially because, as the code is written above, the lists module is imported for each recursive call to bsort. For the purpose of this paper, we will assume that importing code which is already imported will have no cost. This is sensible from our theoretical viewpoint because the sequent Γ, D ⟶ D ⊃ G is provable from the sequent Γ, D ⟶ G.

For the convenience of later examples, we introduce the following definitions. Let the notation P(x̄) denote a finite set of definite clauses all of whose free variables are in the variable list x̄. Let the symbols M, M_{1}, M_{2}, M_{3} be the names of modules. These symbols, just like function and predicate symbols, have an arity and take arguments. The arguments of a module name are used to designate the formal parameters of that module. For our purposes here, the meaning of a module, say M(x̄), is some set of definite clauses P(x̄). This association between module names and definite clauses can be established by the following syntactic specifications:

module M_{1}  module M_{2}(x)  module M_{3}(y, z)
import M_{1}, M_{2}(f(y))
P_{1}  P_{2}(x)  P_{3}(z)

The first module is not parametric because the clauses in P_{1} contain no free variables. M_{1} will simply be shorthand for the conjunction of the clauses in P_{1}. The second module is parametric and the clauses P_{2} can contain various free occurrences of the variable x. Finally the third module is both parametric and explicitly imports M_{1} and an instance of M_{2}. The new syntax for importing modules is only a shorthand for writing certain embedded implications. In the sort module above, if bsort had required several clauses, each one of them may have required the lists module as a hypothesis. To save writing this hypothesis for the body of every clause, we introduce this syntax for imports. The intended meaning of module M_{3} is the following: For each clause of the form

∀w̄(G ⊃ A)

in P_{3} replace it with one of the form

∀w̄((M_{1} ∧ M_{2}(f(y)) ⊃ G) ⊃ A),

that is, the body of all clauses in M_{3} are relativized by the imported modules. The resulting clauses are then associated with the module name M_{3}. Of course, variable capture must be avoided here. If y is a member of the list w̄, the bound variables would need to be changed before forming this new clause.

There are two facts that are important to point out about this development of modules. Firstly, this notion of modules is a by-product of our definite clauses. It has not been added as a separate syntactic feature that an interpreter for O-proofs would need to understand. The meaning and use of modules could be reduced to uses of embedded implications. Of course, in practice this reduction would not be done so literally. A structure-sharing mechanism for modules would need to be considered. Secondly, the operational behavior of implications presented earlier is enough to guarantee that whenever a module is imported into another module, the imported module is only used privately. No additional safeguards need to be added to force private usage. In other words, if a module does not explicitly import a given module, it does not have direct access to the code in that module.

A Logical Analysis of Modules 4. Modules as Interfaces

To illustrate this fact, consider the two modules M_{1} which contains just the definite clause p and M_{2} which contains the definite clause q ⊃ p. Clearly, there is no O-proof of M_{2} ⊃ p because there is no way to prove q within M_{2}. If M_{2} were to import M_{1}, there would still be no proof of q in M_{2}. Thus, if M_{2}′ is the module which contains q ⊃ p and imports M_{1}, there should be no O-proof of p from M_{2}′. This is in fact the case. The formula represented by M_{2}′ is (p ⊃ q) ⊃ p, and it is easy to check that the goal ((p ⊃ q) ⊃ p) ⊃ p has no O-proof. Thus, even though M_{2}′ imports a module which claims that p is true, it is not possible to prove p from that module. That is, M_{1} is used privately within M_{2}′. It is worthwhile noting that the formula ((p ⊃ q) ⊃ p) ⊃ p is often called Peirce’s formula and is well known as a classically true but intuitionistically false formula. The restricted nature of implication in intuitionistic logic is precisely the restriction needed to support private usage of modules when they are imported. In Section 6, we will discuss more about the connections between intuitionistic logic and ⊢_{O}.

As a final example, we give an example of how implication can be used to provide a block structured approach to writing code. The following single definite clause is a definition of the list reverse program.

rev(L,K) :- (all K rev1([],K,K),
            all X all L all K (rev1([X|L],K,ACC) :-
                                rev1(L,K,[X|ACC])))
           => rev1(L,K,[]).

Our syntax for this definite clause cannot, of course, conform to the syntax of [20] because we need to embed quantified expressions in the body of definite clauses. Instead, we used the expression all X P is correspond to the logical notation ∀x P. The only time the code for the rev1 predicate is accessible is during the evaluation of the rev predicate.

4. Modules as Interfaces Modules can also be used to explicitly export and hide program code in other modules.

For example, let module M_{1} contain clauses for the binary predicates p and s and for the trinary predicate r. Consider the following module.

module M_{2}.
import M_{1}.
q(X,Y) :- p(X,Y).
t(X,Y) :- r(f(Y),[],X).

Let M_{0} be some module which imports M_{2}. M_{0} will have access to the code for predicate p but only through the name q. M_{0} will not, however, have access to the code for predicate s since this is not mentioned in M_{2}. Also, only a certain instance of the code for the predicate r is provided by the predicate t. Such an interfacing module is very similar in spirit to what O’Keefe’s called a breeze brick [17].

In this example, we have chosen to export the predicate p in M_{1} as the predicate q. We could have exported p as p. For example, let M_{3} be identical to M_{2}, except that we replace the define clause q(X,Y) :- p(X,Y) with p(X,Y) :- p(X,Y). These clauses are, of course, simply shorthand for the definite clauses ∀x∀y ((M_{1} ⊃ p(x, y)) ⊃ q(x, y)) and ∀x∀y ((M_{1} ⊃ p(x, y)) ⊃ p(x, y)). From an abstract point-of-view, this choice is immaterial; that is, we have the following equalities:

{⟨t, s⟩ | M_{1} ⊢_{O} p(t, s)} = {⟨t, s⟩ | M_{2} ⊢_{O} q(t, s)} = {⟨t, s⟩ | M_{3} ⊢_{O} p(t, s)}.

Proofs for M_{3} ⟶ p(t, s) can be, however, different from those for M_{2} ⟶ p(t, s). For example, consider the following tree of sequents:

∀x∀y ((M_{1} ⊃ p(x, y)) ⊃ p(x, y)), M_{1} ⟶ p(t, s) (6)

∀x∀y ((M_{1} ⊃ p(x, y)) ⊃ p(x, y)) ⟶ M_{1} ⊃ p(t, s) (2).

∀x∀y ((M_{1} ⊃ p(x, y)) ⊃ p(x, y)) ⟶ p(t, s)

The search for an O-proof of p(t, s) from M_{3} gives rise to the search of a proof for p(t, s) from M_{3} and M_{1}. Since M_{3} does not affect the extension of p, this is, in the abstract sense, the same as proving p(t, s) from M_{1}. An interpreter for O-proofs could, however, loop infinitely often by repeatedly using the M_{3} code instead of using the M_{1} code. Exporting p as q is one way to get around this problem. Consider the following tree of sequents:

∀x∀y ((M_{1} ⊃ p(x, y)) ⊃ q(x, y)), M_{1} ⟶ p(t, s) (6)

∀x∀y ((M_{1} ⊃ p(x, y)) ⊃ q(x, y)) ⟶ M_{1} ⊃ p(t, s) (2).

∀x∀y ((M_{1} ⊃ p(x, y)) ⊃ q(x, y)) ⟶ q(t, s)

In this case, an interpreter is forced to examine the code in M_{1}.

Returning to our first example in this section: if p was implemented in M_{1} with calls to the predicate s, only p, exported as q, will be available from M_{2}, not s. Hence, it is possible to hide some aspects of the actual implementation of programs. This is an essential feature in supporting the usual software engineering notion of an abstract datatype.

To illustrate this more directly, consider implementing binary trees which are labeled with integers in such a way that integers labeling the nodes to the left (resp. right) of a given node are smaller (larger) than the label of the given node. The following module represents a particular implementation of inserting and traversing such trees.

module btree_internal.
import lists.
insert_btree(N,bt(N,T1,T2)).

insert_btree(N,bt(M,T,_))  :-
        N < M, insert_btree(N,T).
insert_btree(N,bt(M,_,T))  :-
        N > M, insert_btree(N,T).
traverse_btree(leaf,[]).
traverse_btree(bt(N,L,R), SortedList) :-
        traverse_btree(L,Left), traverse_btree(R, Right),
        append(Left,[N|Right],SortedList).

Here a particular structuring of binary trees is chosen: the term bt(N,T1,T2) represents a non-terminal node labeled with N and which has left-subtree T1 and right-subtree T2. Leaf nodes are represented by the constant leaf.

Such a representation is, of course, largely arbitrary and probably of little significance to the rest of the program using this module. In such a case, it would be desirable to hide the actual implementation of such binary trees. We can do this with the following interfacing module.

module btree.
make_btree(TreeName,Goal) :-
     btree(TreeName,T) => Goal.
insert(TreeName,N)  :-
     btree_internal => (btree(TreeName,T),
                        insert_btree(N,T)).
traverse(TreeName,L) :-
     btree_internal => (btree(TreeName,T),
                        traverse_btree(T,L)).
build(TreeName,[]).
build(TreeName,[X|L]) :-
         insert(TreeName,X), build(TreeName,L).

This module associates binary trees with user supplied names; this association is stored as a “temporary assert” using atomic facts of the form btree(TreeName,Tree). It also provides the basic manipulations (insertions and traversals) for such named trees. The goal

make_btree(TreeName,Goal) will call the goal Goal in an environment where TreeName is

associated with some unspecified binary tree. This tree is initialized as a logical variable. Successive calls to insert are used to add integer labels to this tree. The action of inserting such labels does not produce new copies of the binary tree; the logical variables within the tree are simply specified further. In a sense, this datatype represents monotone binary trees: such trees can grow at the leaves, but once a node is labeled with a value, no change can be made to it. When a binary tree is traversed, all the logical variables in the tree are instantiated to the constant leaf and no further insertions can be made.

The following module describes a sorting procedure which uses the btree datatype.

module btree_sort.
import btree.
binsort(L,K) :- make_btree(sort,(build(sort,L),
                               traverse(sort,K))).

The name sort is the name of a binary tree, and all access to that tree is made through that name. This code is independent of the actual implementation of binary trees. For example, if btree_internal attempted to balance binary trees on certain insertions, the meaning of the above code would not change. A user who imports btree_sort will only have access to the binary predicate binsort. No other code is made available.

The module btree does not explicitly import the module btree_internal: it was imported only locally in two of its three clauses. If btree_internal had been imported over all three clauses, then the goal Goal in make_btree(TreeName,Goal) would have been given access to the internal representation of binary trees. This would defeat the hiding mechanism. The import declaration often provides imported modules with too broad a scope. Explicit uses of => can provide for more selective scoping.

Although this development of abstract datatypes seems to capture many of the standard software engineering notion of abstract datatypes, it does not capture all of them. For example, modules do not provide a perfect hiding mechanism. It is always possible to get at the internal structure of data objects by guessing at their implementation. For example, some module could reimplement the code within btree_internal and thus gain access to the representation of binary trees. Also, by simply issuing the goal btree(Name,Tree) in the right context, a user could get access to all the stored binary trees. Of course, this user would need to know the fact that they were stored in this fashion. It would seem that supporting a greater degree of security for abstract datatypes would require further extensions to either the logic or control primitives of the programming language we are investigating. In [15] we present a further extension to definite clauses, namely the addition of universally quantified goals, which can be used to hide access to term constructors in datatypes. A discussion of this mechanism is beyond the scope of this paper.

The code in two different modules might overlap, i.e., they could both provide definitions for a common predicate. For example, assume modules M_{1} and M_{2} both contain clauses for the binary predicate p. There are occasions when the desired meaning for p is simply the union of the clauses in M_{1} and M_{2}. This would be the case if these modules were parts of a database of facts and we wished to do a simple accumulation of these fact. This could be done with the following query:

⊢_{O} M_{1} ∧ M_{2} ⊃ ∃x∃y p(x, y).

A Logical Analysis of Modules 5. Model Theory

Another way to bring these modules together is to view each one as being different versions of some program. We might then wish to find solutions to p with respect to the version in M_{1} and then with respect to the version in M_{2}. This could be done by first building the module:

module M_{3}.
q(X,Y) :- M_{1} => p(X,Y).
q(X,Y) :- M_{2} => p(X,Y).

and then using the query:

⊢_{O} M_{3} ⊃ ∃x∃y q(x, y).

When a program is placed in a module, it is often the case that we would like to think of that program as being completely defined within that module. That is, in all environments, that module should always have the same meaning. As our one example above showed, it is possible for a second module to be used along with a given module in such a way that the clauses in the two modules accummulate. For some programs, such an addition of foreign clauses could greatly change the original program’s meaning. When this is not desired, it is possible to add control primitives which specify that programs in modules cannot be extended. This could be done by explicitly using a !, fail combination in an interfacing module. For example, consider the following module:

module closedsort(Order).
import sort(Order).
binsort(L1,L2) :- bsort(L1,L2); !, fail.

This small module defines a version of bubble sort which cannot be extended with foreign clauses: a depth-first interpreter could never access them.

There are numerous other observations which could be made about how this notion of module could be used to structure programs and search. We shall now, however, turn away from such concerns to study some of the formal aspects of definite clauses and O-proofs.

5. Model Theory In this section we shall present an alternative description of operational derivability.

We shall do this by constructing a set-theoretic structure, i.e., a kind of model, such that P ⊢_{O} G if and only if G is satisfied in that model. The main challenge to the construction of such a model is the fact that a program may grow during its “execution.” That is, when trying to determine that P ⊢_{O} G holds, it might be necessary to determine that P′ ⊢_{O} G′ holds, where P′ is some extension of P. From the model theory perspective, this means that an interpretation of P would depend on interpretations associated with larger programs.

We therefore use an approach to semantics which is inspired by possible-worlds or Kripke models: we attempt to interpret all programs simultaneously by using a single large Kripkelike interpretation. It is then possible to inductively build a single interpretation which can then be viewed as interpreting all programs. This single interpretation will be the least fixed point of a suitable operator. The references [5] and [19] contain more on Kripke models.

We shall assume that we have chosen a fixed set of non-logical constant, function, and predicate symbols. Let U denote the set of all closed terms (the Herbrand universe) and let H denote the set of all closed, atomic formulas (the Herbrand base). Let W be the set of all programs and let any function I : W → powerset(H) such that ∀w_{1}, w_{2} ∈ W[w_{1} ⊆ w_{2} ⊃ I(w_{1}) ⊆ I(w_{2})] be called an interpretation. An interpretation is simply a mapping which associates to every program a set of “true” atomic formulas which is internally “monotone,” i.e., if a program gets larger, the set of associated true atoms cannot decrease.

We now define each of the following for interpretations I_{1} and I_{2}.

\begin{aligned}I_{1} ⊑ I_{2} & := ∀w ∈ W[I_{1}(w) ⊆ I_{2}(w)] \\ (I_{1} ⊔ I_{2})(w) & := I_{1}(w) ∪ I_{2}(w) \\ (I_{1} ⊓ I_{2})(w) & := I_{1}(w) ∩ I_{2}(w) \end{aligned}

It follows quickly from the fact that the powerset of H is a complete lattice that the set of all interpretations is also a complete lattice under ⊑. In this lattice, ⊔ is the join operator and ⊓ is the meet operator. The smallest interpretation, I_{⊥}, is given by setting I_{⊥}(w) := ∅ for all w ∈ W.

We next define a notion of satisfiability, I, w ⊧ ⊧ G, for closed goal formula G in an interpretation I at a program w.

∘ I, w ⊧ ⊧ A if and only if A ∈ I(w).

∘ I, w ⊧ ⊧ G_{1} ∨ G_{2} if and only if I, w ⊧ ⊧ G_{1} or I, w ⊧ ⊧ G_{2}.

∘ I, w ⊧ ⊧ G_{1} ∧ G_{2} if and only if I, w ⊧ ⊧ G_{1} and I, w ⊧ ⊧ G_{2}.

∘ I, w ⊧ ⊧ ∃x G if and only if I, w ⊧ ⊧ [x/t]G for some t ∈ U.

∘ I, w ⊧ ⊧ D ⊃ G if and only if I, w ∪ {D} ⊧ ⊧ G.

An interpretation can be thought of as a large collection of models which is indexed by programs. Thus, I, w ⊧ ⊧ G means that G is true in the model located in I at program w. The truth of the goal D ⊃ G in the model located at w is given by the truth of the goal G in the model located at w ∪ {D}. This is how the growth of programs is captured.

We now wish to build a single interpretation I such that P ⊢_{O} G if and only if I, P ⊧ ⊧ G. Such an interpretation will be the result of building a least fixed point. To this end, let T be a function from interpretations to interpretations defined as follows:

T (I)(w) := {A | A ∈ [w] or

there is a closed clause G ⊃ A ∈ [w] such that I, w ⊧ ⊧ G}.

It is easy to show that T (I) is an interpretation whenever I is an interpretation.

We first state two lemmas concerning the predicate ⊧ ⊧. Both these lemmas are proved using induction on the structure of goal formulas. We present the proof for only the second lemma. The proof of the first is similar and simpler. Lemma 2. If I_{1} ⊑ I_{2} then I_{1}, w ⊧ ⊧ G implies I_{2}, w ⊧ ⊧ G for all w ∈ W. Lemma 3. Let I_{1} ⊑ I_{2} ⊑ I_{3} ⊑ … be a sequence of interpretations. If G is a goal, w ∈ W, and ⨆_{i=1}^{∞} I_{i}, w ⊧ ⊧ G then there exists a k ≥ 1 such that I_{k}, w ⊧ ⊧ G. Proof. The proof is by induction on the structure of G. If G is atomic, then ⨆_{i=1}^{∞} I_{i}, w ⊧ ⊧ G implies that G ∈ (⨆_{i=1}^{∞} I_{i})(w) = ⋃_{i=1}^{∞} I_{i}(w). Thus there is a k ≥ 1 such that G ∈ I_{k}(w). Hence, I_{k}, w ⊧ ⊧ G. Now assume that for all increasing sequences of interpretations and all w ∈ W, the lemma is true for all goal formulas with a given bounded size. We need to consider the following four cases. Case 1: G = G_{1} ∧ G_{2}. Since ⨆_{i=1}^{∞} I_{i}, w ⊧ ⊧ G_{1} ∧ G_{2}, we have ⨆_{i=1}^{∞} I_{i}, w ⊧ ⊧ G_{1} and ⨆_{i=1}^{∞} I_{i}, w ⊧ ⊧ G_{2}. By the inductive hypothesis, there are two positive integers l and j such that I_{l}, w ⊧ ⊧ G_{1} and I_{j}, w ⊧ ⊧ G_{2}. Let k be the maximum of l and j. By Lemma 2, we have I_{k}, w ⊧ ⊧ G_{1} and I_{k}, w ⊧ ⊧ G_{2}, and therefore I_{k}, w ⊧ ⊧ G_{1} ∧ G_{2}. Case 2: G = G_{1} ∨ G_{2}. Since ⨆_{i=1}^{∞} I_{i}, w ⊧ ⊧ G_{1} ∨ G_{2}, we have ⨆_{i=1}^{∞} I_{i}, w ⊧ ⊧ G_{j} for some j = 1, 2. By the inductive hypothesis, there is a positive integer k such that I_{k}, w ⊧ ⊧ G_{j}. Thus I_{k}, w ⊧ ⊧ G_{1} ∨ G_{2}. Case 3: G = ∃x G′. Since ⨆_{i=1}^{∞} I_{i}, w ⊧ ⊧ ∃x G′, we have ⨆_{i=1}^{∞} I_{i}, w ⊧ ⊧ [x/t]G′ for some t ∈ U. By the inductive hypothesis, there is a positive integer k such that I_{k}, w ⊧ ⊧ [x/t]G′. Thus I_{k}, w ⊧ ⊧ ∃x G′. Case 4: G = D ⊃ G′. Since ⨆_{i=1}^{∞} I_{i}, w ⊧ ⊧ D ⊃ G′, we have ⨆_{i=1}^{∞} I_{i}, w ∪ {D} ⊧ ⊧ G′. By the inductive hypothesis, there is a positive integer k such that I_{k}, w ∪ {D} ⊧ ⊧ G′. Thus I_{k}, w ⊧ ⊧ D ⊃ G′.

Notice that I_{⊥}, P ⊧ ⊧ G holds for no P and G, and that T (I_{⊥}), P ⊧ ⊧ G holds if and only if G is atomic and G ∈ [P]. We now show that T is a monotone and continuous function on the lattice of interpretations. Lemma 4. T is monotone; that is, if I_{1} ⊑ I_{2} then T (I_{1}) ⊑ T (I_{2}). Proof. Assume that I_{1} ⊑ I_{2} and let w ∈ W and A ∈ T (I_{1})(w). Thus either A ∈ [w], in which case A ∈ T (I_{2})(w), or there is a closed clause G ⊃ A ∈ [w] such that I_{1}, w ⊧ ⊧ G. By Lemma 2, I_{2}, w ⊧ ⊧ G so A ∈ T (I_{2})(w). Since w and A were arbitrary, we can conclude that T (I_{1}) ⊑ T (I_{2}).

Lemma 5. T is continuous; that is, if I_{1} ⊑ I_{2} ⊑ I_{3} ⊑ … is a sequence of interpretations, then

⨆_{i=1}^{∞} T (I_{i}) = T (⨆_{i=1}^{∞} I_{i}).

Proof. To prove this equality, we prove inclusion in two directions.

Since I_{j} ⊑ ⨆_{i=1}^{∞} I_{i} for any j, j ≥ 1, we can apply Lemma 4 to get T (I_{j}) ⊑ T (⨆_{i=1}^{∞} I_{i}). Since j was arbitrary, we have ⨆_{i=1}^{∞} T (I_{i}) ⊑ T (⨆_{i=1}^{∞} I_{i}).

Let w ∈ W and A ∈ T (⨆_{i=1}^{∞} I_{i})(w). If A ∈ [w] then A ∈ T (I_{j})(w) for any j, j ≥ 1 and, clearly, A ∈ (⨆_{i=1}^{∞} T (I_{i}))(w). Otherwise, there is a closed clause G ⊃ A ∈ [w] such that ⨆_{i=1}^{∞} I_{i}, w ⊧ ⊧ G. By Lemma 3, there is a k such that k ≥ 1 and I_{k}, w ⊧ ⊧ G. Thus A ∈ T (I_{k})(w) ⊆ (⨆_{i=1}^{∞} T (I_{i}))(w). Since w and A are arbitrary, we conclude that T (⨆_{i=1}^{∞} I_{i}) ⊑ ⨆_{i=1}^{∞} T (I_{i}).

This theorem and proof would remain true if we lifted the restriction that programs were finite. Making programs infinite will not harm the continuity of T.

By the Knaster-Tarski theorem [1], the least fixed point of T is given by the equation

T^{∞}(I_{⊥}) := T (I_{⊥}) ⊔ T^{2}(I_{⊥}) ⊔ T^{3}(I_{⊥}) ⊔ ….

The following theorem can now be proved. Theorem 6. If P is a closed program and G is a closed goal formula, then P ⊢_{O} G if and only if T^{∞}(I_{⊥}), P ⊧ ⊧ G. Proof. First we show that P ⊢_{O} G implies T^{∞}(I_{⊥}), P ⊧ ⊧ G. We do this by showing by induction on k that for all programs P and all closed goal formulas G, if the sequent P ⟶ G has a O-proof of height k then T^{∞}(I_{⊥}), P ⊧ ⊧ G.

Base case: k = 1. G must be atomic and G ∈ [P]. Thus, G ∈ T^{1}(I_{⊥})(P) ⊆ T^{∞}(I_{⊥})(P) and T^{∞}(I_{⊥}), P ⊧ ⊧ G.

Inductive case: k ≥ 1. We need to consider the cases where the last inference in the O-proof of Γ ⟶ G is an instance of inference figure (2) — (6). We present only the cases corresponding to inference figures (2) and (6). The other three cases are straightforward.

Assume that the last inference figure was (2). Then G is atomic and there is a G′ ⊃ G ∈ [P] such that P ⟶ G′ has an O-proof of height k − 1. By the inductive hypothesis, T^{∞}(I_{⊥}), P ⊧ ⊧ G′. By the definition of T, G ∈ T (T^{∞}(I_{⊥}))(P) = T^{∞}(I_{⊥})(P). Hence, T^{∞}(I_{⊥}), P ⊧ ⊧ G.

Assume that the last inference figure was (6). Thus G is of the form D ⊃ G′ and P, D ⟶ G′ has an O-proof of height k − 1. By the inductive hypothesis, T^{∞}(I_{⊥}), P ∪ {D} ⊧ ⊧ G′. Hence, T^{∞}(I_{⊥}), P ⊧ ⊧ D ⊃ G′.

A Logical Analysis of Modules 6. Proof Theory

We now prove the converse. Let P and G be such that T^{k}(I_{⊥}), P ⊧ ⊧ G for some k ≥ 1 and assume that this is the smallest such value for k. If G contains n ≥ 0 occurrences of logical connectives and quantifiers, we then attach to the pair P, G the ordinal measure ω · (k − 1) + n. We now prove by induction on this measure that for all programs P and all closed goal formulas G, if the measure of the pair P, G is α then P ⊢_{O} G.

Base case: the measure of P, G is 0 (= ω · 0 + 0). G is, therefore, atomic and T^{1}(I_{⊥}), P ⊧ ⊧ G. But then G ∈ [P] and P ⊢_{O} G.

Inductive case: the measure of P, G is ω · α + β > 0. This case must be divided between the case where this ordinal is a limit ordinal or not, i.e., β = 0 or β > 0.

Subcase β = 0. Hence, α > 0 and G is atomic. Thus T^{α+1}(I_{⊥}), P ⊧ ⊧ G and G ∈ T^{α+1}(I_{⊥})(P). By the definition of T, either G ∈ [P], in which case P ⊢_{O} G is immediate, or there is a closed G′ ⊃ G ∈ [P] such that T^{α}(I_{⊥}), P ⊧ ⊧ G′. In the second case, the ordinal ω · (α − 1) + β′, where β′ is the number of logical connectives in G′, is smaller than ω · α + β. By the inductive hypothesis, P ⊢_{O} G′ has an O-proof, so P ⊢_{O} G has an O-proof by proof rule (2).

Subcase β > 0. In this case, G is not atomic. This part of the proof, therefore, breaks into four cases, one for each possible top-level connective of G. The proof of each of these cases is straigthforward and omitted here.

Finally, if T^{∞}(I_{⊥}), P ⊧ ⊧ G, by Lemma 3, there is a k ≥ 1 such that T^{k}(I_{⊥}), P ⊧ ⊧ G. Hence, the pair P, G has a measure and by the preceding inductive proof, this implies that P ⊢_{O} G.

A similar theorem for the classical theory of positive Horn clauses is given in [1]. The fixed point result in that paper can be viewed as a special case of Theorem 6.

6. Proof Theory At this point, we would like to know if our programming language represents a new

logical system or if it is an instance of some other known logical system. The purpose of this section is to address this question.

It is worthwhile noting that our emphasis here is different than what is generally found in theoretical discussions of logic programming. The more common approach starts with a specific logic, namely classical first-order logic, and then examines the programming language significance of that logic’s meta-theory. Our approach in this paper is the reverse, that is, we first fixed a natural and interesting programming language and then looked for a logic whose meta-theory includes its operational semantics. This step of looking for such a logic is not meant to justify the programming language — it is justified to the extent that it has formal properties and implements important programming features. We wish instead to discover if our logic has been studied previously in the logic literature.

We have already mentioned that if ⊢_{O} represents a provability relation in some logic, that logic cannot be classical logic. For another illustration of this, consider the goal formula G_{1} ∨ (D ⊃ G_{2}). Our operational semantics interprets this goal as one which will succeed if either G_{1} succeeds or if G_{2} succeeds given the program in D. The scope of D is clearly over only G_{2}. Classical logic, however, does not support this interpretation of this goal. For example, in classical logic, the following equivalences are tautologous:

G_{1} ∨ (D ⊃ G_{2}) ≡ G_{1} ∨ ∼D ∨ G_{2}
≡ ∼D ∨ G_{1} ∨ G_{2}
≡ (D ⊃ G_{1}) ∨ G_{2}
≡ (D ⊃ G_{1}) ∨ (D ⊃ G_{2})

The classical equivalence of p ⊃ q with ∼p ∨ q undermines the intended meaning of implication as providing an environment building mechanism. We will show how two weaker logics, minimal logic and intuitionistic logic, can be used to provide a justification for our intended interpretation of the logical connectives.

We now present a different set of inference figures for sequents than those introduced in Section 1. This proof system is taken from [18].

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

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

\begin{aligned}B, Γ ⟶ Θ, C \\ & ⊃-R \\ Γ ⟶ Θ, B ⊃ C \end{aligned}

Γ, [x/t]P ⟶ Θ ; ∀-L ; Γ, ∀x P ⟶ Θ  Γ ⟶ Θ, [x/t]P ; ∃-R ; Γ ⟶ Θ, ∃x P

Γ, [x/y]P ⟶ Θ ; ∃-L ; Γ, ∃x P ⟶ Θ  Γ ⟶ Θ, [x/y]P ; ∀-R ; Γ ⟶ Θ, ∀x P

\begin{aligned}Γ ⟶ Θ, ⊥ \\ & ⊥-R \\ Γ ⟶ Θ, B \end{aligned}

The proviso that the variable y is not free in any formula of the lower sequent is also assumed for the ∃-L and ∀-R figures.

A proof for the sequent Γ ⟶ Θ is a finite tree constructed using these inference figures and such that the root is labeled with Γ ⟶ Θ and the leaves are labeled with initial sequents, i.e., sequents Γ ⟶ Θ such that the intersection Γ ∩ Θ contains either ⊥ or an atomic formula.

Sequent systems of this kind generally have three structural figures which we have not listed. Two such figures, interchange and contraction, are not necessary here because the antecedents and succedents of sequents are sets instead of lists. Hence, the order and multiplicity of formulas in sequents are not made explicit. If an antecedent is of the form Γ, B, it may be the case that B ∈ Γ; that is, a formula in an antecedent or succedent has an arbitrary multiplicity. The third common structural inference figure is that of thinning: from a given sequent one may add any additional formulas to the succedent and antecedent. The following lemma, which can be proved easily by induction, establishes a form of antecedent thinning which we will find useful. We will not, however, introduce thinning as a separate inference figure.

Lemma 7. Let Ξ be a proof of Γ ⟶ Θ and let Γ′ be a set of formulas. Let Ξ + Γ′ be the tree of sequents obtained by adding Γ′ to the antecedent of all sequents in Ξ. Then Ξ + Γ′ is a proof for Γ ∪ Γ′ ⟶ Θ.

We define the following three kinds of proofs. Any proof will also be called a Cproof. Any C-proof such that every sequent in it has a singleton set for it succedent is also called an I-proof. Furthermore, an I-proof in which no instance of the ⊥-R inference figure appears is also called an M-proof. Sequent proofs in classical C, intuitionistic I, and minimal M logics are represented by, respectively, by C-proofs, I-proofs, and M-proofs. Finally, we write Γ ⊢_{C} B, Γ ⊢_{I} B, and Γ ⊢_{M} B, if the sequent Γ ⟶ B has, respectively, a C-proof, I-proof, or M-proof. It follows immediately that Γ ⊢_{M} B implies Γ ⊢_{I} B implies Γ ⊢_{C} B. If the set Γ is empty, it will be dropped entirely from the left side of these three predicates. See [5, 9, 18, 21] for more on intuitionistic and minimal logics.

The following is a C-proof for a formula we considered in Section 1.

\begin{aligned}p(a), p(b) ⟶ p(a) & p(a), p(b) ⟶ p(b) \\ & ∧-R \\ p(a), p(b) ⟶ p(a) ∧ p(b) \end{aligned} p(a), p(b), q ⟶ q ⊃-L

p(a) ∧ p(b) ⊃ q, p(a), p(b) ⟶ q ⊃-R

p(a) ∧ p(b) ⊃ q, p(a) ⟶ q, p(b) ⊃ q ⊃-R

p(a) ∧ p(b) ⊃ q ⟶ p(a) ⊃ q, p(b) ⊃ q ∃-R

p(a) ∧ p(b) ⊃ q ⟶ p(a) ⊃ q, ∃x (p(x) ⊃ q) ∃-R.

p(a) ∧ p(b) ⊃ q ⟶ ∃x (p(x) ⊃ q)

Similarly, the following is a C-proof of Peirce’s formula, mentioned at the end of Section 3.

\begin{aligned}p ⟶ p, q \\ & ⊃-R \\ ⟶ p, p ⊃ q \end{aligned} p ⟶ p ⊃-L

(p ⊃ q) ⊃ p ⟶ p ⊃-R.

⟶ ((p ⊃ q) ⊃ p) ⊃ p

Neither of these formulas have I-proofs.

In classical proofs, there may be more than one formula in the succedent, and the “processing” of any one of these formulas may interact with the others in the succedent. This is very clear if we return to the goal formula, G_{1} ∨ (D ⊃ G_{2}), presented earlier. Consider the following tree of sequents:

D ⟶ G_{1}, G_{2} ⊃-R

⟶ G_{1}, D ⊃ G_{2} ∨-R

⟶ G_{1}, G_{1} ∨ (D ⊃ G_{2}) ∨-R

⟶ G_{1} ∨ (D ⊃ G_{2})

This reduction of the root sequent to D ⟶ G_{1}, G_{2} loses the scoping restriction of D over G_{2}. Permitting more than one formula on the right works against our intented interpretation of the logical connectives. Theorem 8. Let P be a set of definite clauses and let G be a goal formula. If P ⊢_{O} G, then P ⊢_{M} G, P ⊢_{I} G, and P ⊢_{C} G. Proof. Each of the inference figures (2) through (6) are derivable in M in the following way. Figure (2) is a combination of ∀-L, ∧-L, ⊃-L, and an initial sequent; figure (3) is ∨-R; figure (4) is ∧-R; figure (5) is ∃-R; figure (6) is ⊃-R. An initial sequent of ⊢_{O} is derivable from ∀-L, ∧-L, and an initial sequents of this system. Since all these inference figures are derivable in the weakest system, M, they are also derivable in I and C.

The proofs of the next two lemmas are straightforward inductions on the height of proofs. Lemma 9. Let P be a set of definite clauses and Θ be a set of goal formulas. Any proof of a sequent P ⟶ Θ contains no instances of the inference figures ∨-L, ∃-L, and ∀-R. Lemma 10. Let P be a set of definite clauses. There is no I-proof of the sequent P ⟶ ⊥.

From Lemma 10 it follows that any I-proof of P ⟶ Θ cannot contain any instances of the ⊥-R inference figure. Hence, for a set of definite clauses P and a goal formula G, P ⊢_{I} G if and only if P ⊢_{M} G.

We now wish to show that if P ⟶ G is intuitionistically provable, it is then operationally provable. There are several overlaps between the O and I proof systems, but there are two substantial differences. First, there are no O-proof inference figures which correspond to ∀-L and ∧-L. This difference is compensated by the use of [P] instead of P in proof rules (1) and (2). Secondly, and more importantly, the match between inference figures (2) and ⊃-L is not direct. Given the sequent G′ ⊃ A, P ⟶ G, (2) is applicable only if G = A while ⊃-L has no such restriction. In fact, ⊃-L generates an entire subproof for A, P ⟶ G which is not present in instances of inference figure (2). As a result of this difference, we need to make the following definitions and observations.

Instances of ⊃-L in a proof are at the root of two smaller proofs. These two proofs are called the left subproof and right subproof of this instance of ⊃-L. An instance of ⊃-L in a proof is simple if its right subproof has height 1. Otherwise, the instance is complex. A proof in which all instances of ⊃-L are simple is a simple proof. It is simple instances of ⊃-L which correspond to uses of inference figure (2). Lemma 12 establishes that simple I-proofs are sufficient. First, however, we need to prove the following lemma. Lemma 11. Assume that Ξ is an I-proof of the form

\begin{matrix}Ξ_{1} \\ P ⟶ G′ \end{matrix}  \begin{matrix}Ξ_{2} \\ A, P ⟶ G \end{matrix} ⊃-L,
G′ ⊃ A, P ⟶ G

where Ξ_{1} and Ξ_{2} are simple I-proofs. There exists a simple I-proof for

G′ ⊃ A, P ⟶ G.

Proof. Our proof shows how a complex instance of ⊃-L can be converted to simple instances by moving it backwards through the inference figures in Ξ_{2}. To do this, we need to show that ⊃-L “commutes” with all inference figures in which Ξ_{2} can terminate. Formally, the proof is by induction on the height of Ξ_{2}. If the height is 1, then the instance of ⊃-L above is simple and we are finished. Assume that the height of Ξ_{2} is greater than 1. We now show that this complex instance of ⊃-L commutes with the last inference figure in Ξ_{2}. We consider the cases for each such inference figure.

Cases ∧-R, ⊃-R, ∨-R, and ∃-R: Assume that the root inference figure in Ξ_{2} is ∧-R. Hence, Ξ is of the form

\begin{matrix}Ξ_{1} \\ P ⟶ G′ \end{matrix}  \begin{aligned}\begin{matrix}Ξ′_{2} \\ A, P ⟶ G_{1} \end{matrix} & \begin{matrix}Ξ′′_{2} \\ A, P ⟶ G_{2} \end{matrix} \\ & ∧-R \\ A, P ⟶ G_{1} ∧ G_{2} \end{aligned} ⊃-L.
G′ ⊃ A, P ⟶ G_{1} ∧ G_{2}

Consider the following I-proof:

\begin{aligned}\begin{matrix}Ξ_{1} \\ P ⟶ G′ \end{matrix} & \begin{matrix}Ξ′_{2} \\ A, P ⟶ G_{1} \end{matrix} \\ & ⊃-L \\ G′ ⊃ A, P ⟶ G_{1} \end{aligned} \begin{aligned}\begin{matrix}Ξ_{1} \\ P ⟶ G′ \end{matrix} & \begin{matrix}Ξ′′_{2} \\ A, P ⟶ G_{2} \end{matrix} \\ & ⊃-L \\ G′ ⊃ A, P ⟶ G_{2} \end{aligned} ∧-R.
G′ ⊃ A, P ⟶ G_{1} ∧ G_{2}

The two instances of ⊃-L above both have left and right subproofs which are simple and are such that their right subproofs are shorter than Ξ_{2}. The inductive hypothesis can be applied to each subproof to finish this case. The case when the last inference figure of Ξ_{2} is either ⊃-R, ∨-R, or ∃-R is similar.

Cases ∀-L and ∧-L: Assume that the root inference figure in Ξ_{2} is ∀-L. Hence, Ξ is of the form

\begin{matrix}Ξ_{1} \\ ∀x D, P′ ⟶ G′ \end{matrix}  \begin{matrix}Ξ′_{2} \\ A, [x/t]D, P′ ⟶ G \end{matrix} ; ∀-L ; A, ∀x D, P′ ⟶ G ⊃-L,
G′ ⊃ A, ∀x D, P′ ⟶ G

where P = P′ ∪ {∀x D}. Consider the following I-proof:

\begin{matrix}Ξ_{1} + \{[x/t]D\} \\ [x/t]D, ∀x D, P′ ⟶ G′ \end{matrix}  \begin{matrix}Ξ′_{2} + \{∀x D\} \\ A, [x/t]D, ∀x D, P′ ⟶ G \end{matrix} ⊃-L

G′ ⊃ A, ∀x D, [x/t]D, P′ ⟶ G ∀-L.

G′ ⊃ A, ∀x D, P′ ⟶ G

The instance of ⊃-L above has left and right subproofs which are simple and is such that its right subproof is shorter than Ξ_{2}. The inductive hypothesis can be applied to this instance of ⊃-L to finish this case. The case when the last inference figure of Ξ_{2} is ∧-L is similar.

Case ⊃-L: For our final case, assume that the last inference figure of Ξ_{2} is ⊃-L. Ξ is then of the form

\begin{matrix}Ξ_{1} \\ G_{1} ⊃ A_{1}, P′ ⟶ G′ \end{matrix}  \begin{aligned}\begin{matrix}Ξ′_{2} \\ A, P′ ⟶ G_{1} \end{matrix} & A, A_{1}, P′ ⟶ G \\ & ⊃-L \\ A, G_{1} ⊃ A_{1}, P′ ⟶ G \end{aligned} ⊃-L,
G′ ⊃ A, G_{1} ⊃ A_{1}, P′ ⟶ G

where P = {G_{1} ⊃ A_{1}} ∪ P′. Since, the upper most instance of ⊃-L is simple, the sequent A, A_{1}, P′ ⟶ G is initial. Hence, either G ∈ P′, G = A, or G = A_{1}. If G ∈ P′ then a simple I-proof for the sequent

G′ ⊃ A, G_{1} ⊃ A_{1}, P′ ⟶ G

is the one node proof labeled with just this sequent. If G = A, then a simple I-proof for this sequent would be

\begin{matrix}Ξ_{1} \\ G_{1} ⊃ A_{1}, P′ ⟶ G′ \end{matrix}  A, G_{1} ⊃ A_{1}, P′ ⟶ G ⊃-L.
G′ ⊃ A, G_{1} ⊃ A_{1}, P′ ⟶ G

Finally, if G = A_{1}, then consider the following I-proof:

\begin{aligned}\begin{matrix}Ξ_{1} \\ G_{1} ⊃ A_{1}, P′ ⟶ G′ \end{matrix} & \begin{matrix}Ξ′_{2} + \{G_{1} ⊃ A_{1}\} \\ A, G_{1} ⊃ A_{1}, P′ ⟶ G_{1} \end{matrix} \\ & ⊃-L \\ G′ ⊃ A, G_{1} ⊃ A_{1}, P′ ⟶ G_{1} \end{aligned} A_{1}, G′ ⊃ A, P′ ⟶ G ⊃-L.
G′ ⊃ A, G_{1} ⊃ A_{1}, P′ ⟶ G

The lower instance of ⊃-L is simple while the upper instance is not necessarily simple. Since that instance’s right subproof is shorter than Ξ_{2}, the inductive hypothesis can be used to complete this case.

Lemma 12. Let P be a set of definite clauses and let G be a goal formula. If P ⟶ G has an I-proof, it has a simple I-proof. Proof. This follows by induction on the number of complex instances of ⊃-L in an Iproof of P ⟶ G. If the number of such instances is greater than 0, choose one which has only simple left and right subproofs. Using the preceding lemma, that instance can be removed. The resulting I-proof has one fewer complex instances. In this fashion, all complex instances can be removed.

Theorem 13. Let P be a set of definite clauses and let G be a goal formula. P ⊢_{O} G if and only if P ⊢_{M} G if and only if P ⊢_{I} G. Proof. We need only show one remaining implication, namely, if P ⊢_{I} G then P ⊢_{O} G. We first prove by induction on the height of Ξ that if Ξ is a simple I-proof for P′ ⟶ G and [P′] ⊆ [P], then there exists an O-proof for P ⟶ G. We may assume that no internal sequents in Ξ are instances of initial sequents, since if there was such a sequent, the proof could be simplified by removing the subproofs above it. If the height of Ξ is one, i.e., it is simply an initial sequent, then G is atomic and G ∈ [P′]. Hence, G ∈ [P], and P ⟶ G is an initial sequent for ⊢_{O}. This single sequent is the desired O-proof.

Now assume that the height of Ξ is greater than 1, and let Ξ_{1} and, if necessary Ξ_{2}, be the I-proofs which arise from deleting the last inference figure of Ξ. We need to consider the following 7 cases — one for each inference figure in which Ξ can terminate.

Cases ∨-R, ∧-R, ∃-R: Let the last inference figure of Ξ be ∧-R. Here, G is G_{1} ∧ G_{2}; so Ξ_{1} is a proof of P′ ⟶ G_{1} and Ξ_{2} is a proof of P′ ⟶ G_{2}. By the inductive hypothesis, let T_{1} and T_{2} be O-proofs for, respectively, P ⟶ G_{1} and P ⟶ G_{2}. The necessary O-proof for P ⟶ G_{1} ∧ G_{2} results from appending the inference figure (4) to the trees T_{1} and T_{2}. The cases for ∨-R and ∃-R are similar. These cases use inference figures (3) and (5), respectively, instead of (4).

Case ⊃-R: Let the last inference figure of Ξ be ⊃-R. Here, G is D ⊃ G_{1}; so Ξ_{1} is a proof of P′, D ⟶ G_{1}. By the inductive hypothesis, let T_{1} be an O-proof for P, D ⟶ G_{1}. We may apply the inductive hypothesis since [P′] ⊆ [P] implies [P′, D] ⊆ [P, D]. The necessary O-proof for P ⟶ D ⊃ G_{1} results from appending the inference figure (6) to T_{1}.

Cases ∀-L and ∧-L: Let the last inference figure of Ξ be ∀-L. Hence, P′ = {∀x D}∪P′′, for some set P′′, and Ξ_{1} is a proof of P′′, [x/t]D ⟶ G, for some term t. The inductive hypothesis immediately supplies the necessary O-proof for P ⟶ G. We may apply the inductive hypothesis since [P′] ⊆ [P] implies [P′′, [x/t]D] ⊆ [P]. The case for inference figure ∧-L is similar.

Case ⊃-L: Let the last inference figure of Ξ be ⊃-L. Hence, P′ = {G′ ⊃ A} ∪ P′′ for some P′′. Ξ must then be of the form:

\begin{matrix}Ξ_{1} \\ P′′ ⟶ G′ \end{matrix}  \begin{matrix}Ξ_{2} \\ A, P′′ ⟶ G \end{matrix} ⊃-L.
G′ ⊃ A, P′′ ⟶ G

Since Ξ is simple, A, P′ ⟶ G must be an initial sequent. This forces G = A, since otherwise G ∈ P′′ and the root sequent of Ξ would be an initial sequent, contradicting our assumption about Ξ. By the inductive hypothesis, let T_{1} be an O-proof for P ⟶ G′. We may apply the inductive hypothesis since [P′] ⊆ [P] implies [P′′] ⊆ [P]. Since G′ ⊃ A ∈ P′, G′ ⊃ A ∈ [P] and the necessary O-proof results from appending an instance of the inference figure (2) to T_{1}.

Finally, let P ⊢_{I} G. Then P ⟶ G has a simple I-proof. By the proof above and since [P] ⊆ [P], P ⟶ G has an O-proof and P ⊢_{O} G.

A Logical Analysis of Modules 7. Minimal Logic Negation

Throughout this section, the differences between minimal logic and intuitionistic logic proofs were not evident. This is because goal formulas and definite clauses contain no instances of negations or ⊥. In the next section, we introduce negation to our programming logic. As we shall see, there are two natural interpretation of this negation; one interpretation is equivalent to minimal logic and the other to intuitionistic logic.

7. Minimal Logic Negation Let us now permit the logical constant ⊥ to occur in both goals and definite clauses as

if it were considered an atomic formula. More precisely, for this section, consider definite clauses and goal formulas to be defined by the following mutually recursive definition:

D := ⊥ | A | G ⊃ A | G ⊃ ⊥ | ∀x D | D_{1} ∧ D_{2},
G := ⊥ | A | G_{1} ∧ G_{2} | G_{1} ∨ G_{2} | ∃xG | D ⊃ G.

Formulas of the form B ⊃ ⊥ will be abbreviated as ∼B. Thus, the negation of a goal formula is a definite clause, and the negation of a definite clause is a goal formula. Operationally, let us treat ⊥ just as if it was an atomic formula. Hence, with this simple or “minimal” view of ⊥, we can easily add the following two proof rules to handle the case where ⊥ is a goal.

(7) P ⊢_{O} ⊥ if ⊥ ∈ [P].

(8) P ⊢_{O} ⊥ if there is a formula (G ⊃ ⊥) ∈ [P] and P ⊢_{O} G. We need to add to the O-proof system two inference figures corresponding to (7) and (8). This extension, however, is really not an extension at all. A reasonable implementation of rules (1) — (8) would, in fact, treat ⊥ as a non-logical predicate symbol and simply use rules (1) — (6).

Proof rule (8) asserts that ⊥ follows from P if there is a formula G for which both ∼G ∈ [P] and G follows from P. For this reason, we shall say that P is inconsistent if P ⊢_{O} ⊥. If P is not inconsistent, it is consistent.

The inconsistency of a set of definite clauses P does not necessarily mean that P Oproves all (goal) formulas. For example, It is very easy to show that p ∧ ∼p ⊢_{O} ⊥ while it is not the case that p∧∼p ⊢_{O} q. Hence, inconsistencies are essentially “local.” As the next theorem shows, this view of negation is that of minimal logic and not that of intuitionistic logic. Theorem 14. P ⊢_{O} G if and only if P ⊢_{M} G. There are goals, for example (p ∧ ∼p) ⊃ q, which are intuitionistically provable but not provable in O. Proof. Let Ξ be an O-proof for P ⟶ G. Let Ξ′, P′, and G′ be the result of replacing every instance of ⊥ in Ξ, P, and G by some 0-ary predicate symbol, say F, which does not occur in Ξ. Clearly, Ξ′ is an O-proof of the sequent P′ ⟶ G′. By Theorem 13, there is an M-proof, T for this same sequent. Finally, if we replace all the occurrences of F with ⊥ in T to get T′, then T′ is an M-proof for P ⟶ G. The proof of the converse is similar.

It is a simple matter to strengthen the proof system O so that ⊥ and negation are equivalent to that of intuitionistic logic. This is done by adding a proof rule which encodes the ⊥-R inference figure. That is, we need to add the rule which says that any goal formula is provable if ⊥ is provable. Let O′ be the proof system which is the result of adding the following proof rule to those of O.

(9) P ⊢_{O′} G if P ⊢_{O′} ⊥. It is easy to see, in fact, that p, ∼p ⊢_{O′} q. In fact, we have the following theorem. Theorem 15. P ⊢_{O′} G if and only if P ⊢_{I} G. Proof. The proofs for Lemmas 11 and 12 and for Theorem 13 can be extended to deal with I-proofs which contain the inference figure ⊥-R. These extended lemmas and theorem prove this theorem because proof rule (9) corresponds exactly to ⊥-R for I-proofs.

The choice of which interpretation of ⊥ and negation that is made would seem to depend very much on what applications are written in this language. In an application where it is very important to know whenever a program becomes inconsistent, the minimal logic interpretation is probably the most appropriate. In such a case, it might seem meaningless to be deriving all goal formulas from a program which is inconsistent. Such an application would probably be more concerned with dealing with the inconsistency itself than with continuing to do inferencing with it. On the other hand, if there are some reasoning processes which involve many instances of assuming hypotheses during a single process, then the intuitionistic interpretation might be more natural. This is because the construction of nested proofs often makes use of contradictions to help draw conclusions. For example, the goal formula

((∼p ⊃ r) ⊃ q) ⊃ (p ⊃ q)

has an I-proof but no M-proof. The proof of this goal contains a subproof which proves a contradiction. That contradiction does not, however, reflect on the environment in which the query is initially asked.

For the rest of this paper, we shall assume that we are using the minimal logic interpretation of ⊥.

One way to model negation in a logic programming system is through a meta-logical principle called negation-by-failure. This principle states that a closed atom can be taken as being false if there is no proof of it. While the negation-by-failure principle is much stronger than either the minimal logic or intuitionistic logic interpretation of negation, we can make a useful partial connection between them. If P is consistent and P ⊢_{O} ∼A then there can be no proof of A from P. In a consistent program, therefore, P ⊢_{O} ∼A implies not(A) (negation-by-failure). This suggests the possibility of replacing certain forms of negation-by-failure with the search for proofs of negations. Negation-by-failure is not completely removed from this consideration because determining that a program is consistent requires determining that there is no proof of ⊥. The following example demonstrates these two negation principles.

Let us consider a very simple database program. Facts within our database will be simple, closed atomic formulas. Definite clauses of the form G ⊃ ⊥ will be used to represent constraints. For example, consider the following few clauses.

enrolled(jane,102).
enrolled(bill,100).
⊥ :- enrolled(X,101),enrolled(X,102).

This tiny database asserts that Jane and Bill are/have been enrolled in 102 and 100, respectively. There is also a constraint that states that it is inconsistent for the same person to be enrolled in both 101 and 102. Now consider the following simple database program.

db :- read(Command), do(Command), db.
do(enter(Fact)) :- Fact => db.
do(retract) :- fail.
do(commit) :- repeat.
do(check(Query)) :-
   (Query, write(yes),nl,!;
    Query => ⊥,write(no),nl,!;
    write('no, but it could be true'),nl).
do(consis) :- (not ⊥, write(yes),!; write(no)), nl.

Here, db represents a looping database query and updating program. Providing the command enter(Fact) to db makes an update to the current database by calling db after it has made Fact a hypothesis. It is possible to retract such updates by using the retract command. This command simply fails. All updates will be undone backwards to the point of the last commit command. The commit command will always re-succeed (given, of course, a depth-first interpreter).

A Logical Analysis of Modules 8. Removing Disjunctions From Programs

It is the check command which is most interesting here. It has a three-valued behavior. Assume that the database is consistent. The command check(Query) will first look for a proof of Query, and if one is found, prints “yes”. Otherwise, a proof for the negation of Query, i.e., Query => ⊥ is searched for. (This goal means: “if Query were true, do we have an inconsistency?”) If a proof is found, then “no” is printed. If neither the positive nor negative form of Query can be proved, then the database does not contain Query although it is consistent for Query to be a fact in some extension of that database. If the current database is inconsistent, the conclusions drawn by the check command could be wrong. With respect to the above database, the three commands

check(enrolled(jane,102))
check(enrolled(jane,101))
check(enrolled(bill,101))

would print the answers “yes,” “no,” and “no, but it could be true,” respectively.

The consis command uses negation-by-failure to determine if the current database is consistent. The use of not here is meta-logical and not accounted for by the theory we have presented.

The model presented in Section 5 is rich enough to model this three valued behavior. Let P be a consistent program and let A be a closed atom. Clearly we have either A ∈ T^{∞}(I_{⊥})(P) or A ∉ T^{∞}(I_{⊥})(P). The first case is true when check(A) prints “yes.” The later case, however, can be broken into two additional cases. Clearly, there is some program larger than P in which A is true (P ∪ {A}, for example). Given our classification of worlds into consistent and inconsistent, we can make further distinctions: Either the only extensions of the world P which contain A are inconsistent, or this is not so. The first case is true when check(A) prints “no,” and the later case is true when check(A) prints “no, but it could be true.”

8. Removing Disjunctions From Programs

In this section, we show that disjunctions are not needed in writing programs. That is, for every program there is a second program, generally much larger, which proves the same atomic formulas and which contains no occurrences of disjunctions. This is true for simple Horn clauses as well as definite clauses.

We define two functions, dnf which maps goal formulas to sets of goal formulas, and dfnf which maps definite clauses to sets of definite clauses, by mutual recursion. The expressions ⋀ B and ⋁ B denote, respectively, the conjunction and disjunction of the formulas in B in some fixed but arbitrary order. The two acronyms, dnf and dfnf, stand for the disjunctive normal form and the disjunction-free normal form, respectively. These are defined as follows:

dnf(A) = dfnf(A) = {A}
dnf(G_{1} ∨ G_{2}) = dnf(G_{1}) ∪ dnf(G_{2})
dnf(G_{1} ∧ G_{2}) ={G′ ∧ G′′ | G′ ∈ dnf(G_{1}), G′′ ∈ dnf(G_{2})}
dnf(∃x G) ={∃x G′ | G′ ∈ dnf(G)}
dnf(D ⊃ G) ={(⋀ dfnf(D)) ⊃ G′ | G′ ∈ dnf(G)}
dfnf(G ⊃ A) ={G′ ⊃ A | G′ ∈ dnf(G)}
dfnf(D_{1} ∧ D_{2}) = dfnf(D_{1}) ∪ dfnf(D_{2})
dfnf(∀x D) ={∀x D′ | D′ ∈ dfnf(D)}

If P is a set of definite clauses, then we shall also write dfnf(P) = ⋃{dfnf(D) | D ∈ P}. It is easy to see that the formulas in the sets dnf(G) and dfnf(P) contain no occurrences of disjunctions. The following Lemma has a straightforward proof which is omitted. Lemma 16. Let P be a set of definite clauses. Then each of the following is true.

(1) A ∈ [P] if and only if A ∈ [dfnf(P)].

(2) G ⊃ A ∈ [P] if and only if G′ ⊃ A ∈ [dfnf(P)] for each G′ ∈ dnf(G).

(3) G′ ∈ dnf([x/t]G) if and only if there is a ∃x G′′ ∈ dnf(∃x G) such that G′ = [x/t]G′′. The main result concerning dnf and dfnf is given by the following theorem.

Theorem 17. P ⟶ G has an O-proof if and only if for some G′ ∈ dnf(G), dfnf(P) ⟶ G′ has an O-proof. Proof. Let Ξ be an O-proof for P ⟶ G. We proceed by induction on the height of Ξ.

Case: Ξ is an initial sequent. In that case, G is atomic and G ∈ [P]. By Lemma 16, G ∈ [dfnf(P)] and dfnf(P) ⟶ G is also an initial sequent.

Case: Ξ ends in inference figure (2). Thus, G is atomic and there is a G′ ⊃ G ∈ [P] such that P ⟶ G′ has a shorter O-proof. By the inductive hypothesis, there is a G′′ ∈ dnf(G′), such that dfnf(P) ⟶ G′′ has an O-proof. Again, by Lemma 16, G′′ ⊃ G ∈ [dfnf(P)], so dfnf(P) ⟶ G has an O-proof.

Case: Ξ ends in inference figure (3). Thus, G is a disjunction, G_{1}∨G_{2}, and for i = 1 or i = 2, P ⟶ G_{i} has a shorter O-proof. Hence, for some G′ ∈ dnf(G_{i}), dfnf(P) ⟶ G′ has an O-proof. Since G′ ∈ dnf(G), we are finished.

Case: Ξ ends in inference figure (4). Thus, G is a conjunction, G_{1} ∧ G_{2}, and for i = 1 and i = 2, P ⟶ G_{i} has a shorter proof than Ξ. By the inductive hypothesis, there are formulas G′_{1} ∈ dnf(G_{1}) and G′_{2} ∈ dnf(G_{2}) such that dfnf(P) ⟶ G′_{1} and dfnf(P) ⟶ G′_{2} have O-proofs. Thus, dfnf(P) ⟶ G′_{1} ∧ G′_{2} also has an O-proof. Since G′_{1} ∧ G′_{2} ∈ dnf(G), we are finished.

A Logical Analysis of Modules 9. Related Work

Case: Ξ ends in inference figure (5). Thus, G is an existentially quantified formula, ∃x G_{0}, and for some term t, P ⟶ [x/t]G_{0} has a shorter O-proof. Hence, for some G′ ∈ dnf([x/t]G_{0}), dfnf(P) ⟶ G′ has an O-proof. By Lemma 16, G′ is of the form [x/t]G′′, where ∃x G′′ ∈ dnf(∃x G_{0}). This completes this case.

Case: Ξ ends in inference figure (6). Thus, G is an implication, say D ⊃ G_{0}. Since P, D ⟶ G_{0} has a smaller O-proof, there is a G′ ∈ dnf(G_{0}) such that dfnf(P, D) ⟶ G′ has an O-proof. Since dfnf(P, D) = dfnf(P)∪dfnf(D), the sequent dfnf(P), ⋀ dfnf(D) ⟶ G′ has an O-proof. By applying an instance of inference figure (6) to this proof, we have an O-proof for dfnf(P) ⟶ [⋀ dfnf(D)] ⊃ G′. Since [⋀ dfnf(D)] ⊃ G′ ∈ dnf(G), we have completed this case.

The proof of the converse is similar and is omitted.

A simply corollary of this Theorem is that the two programs P and dfnf(P) prove the same atomic formulas.

9. Related Work Many of the results in this paper were first presented in [12]. The papers [13] and

[15] are direct extensions of the logic presented in this paper. In particular, they introduce a class of formulas, call hereditary Harrop formulas, which properly contains both Horn clauses and the logic of this paper. Hereditary Harrop formulas can be defined for both first-order and higher-order logic.

Gabbay and Reyle in [7] have described a logical language very similar to the one presented here. Their motivation for selecting this logic was largely based on the observation that this language captures more of its own metatheory. For example, the demo predicate of [2] could be encoded directly using implication. That is, the goal, demo(D, G), which should succeed if the goal G is provable from D, is equivalent to the goal D ⊃ G.

Warren in [22] investigated a simpler version of this logic as a basis of a “pure” implementation of a database updating program, such as the one in Section 7. He essentially used implications within goals only when the hypothesis of that implication is atomic. His “modal” operator assume(A)@G notation could be approximated within our language as A ⊃ G. Warren also provides a semantics for this operator using possible worlds semantics.

A stronger logical language, which includes full intuitionistic negation and goals which are universally quantified, is investigated by McCarty in [11]. McCarty uses this logic not in a programming language context but as the basis for building knowledge representation and common sense reasoning programs. He also presents a fixed point construction and a tableau proof procedure for his logic.

Several papers have dealt with designing modules for logic programming languages. For example, Bowen and Weinberg in [3] have extend the work of Bowen and Kowalski in [2] and presented several very interesting programs using a notion similar to modules. Chomicki and Minsky in [4] have shown the importance of introducing modularity into Prolog programs and developed a rule-based security system for controlling access among various fragments of code. Neither of these papers, however, provided a logical analysis of their respective notions of modules. The theoretical results in this paper should provide a basis for such an analysis.

O’Keefe in [17] presents a formal approach to developing modules for Prolog. Much of what he presents in that paper can be captured by the theory presented in this paper. See, for example, our earlier discussion in Section 4 regarding breeze bricks. Nait Abdallah in [16] presents a logical approach to introducing module-like procedures. His approach is to base logic programming within a fragment of second-order logic and to use secondorder quantifiers as an abstraction mechanism for procedures (predicates). This approach is quite different from our development here and to our other work on higher-order logic programming [14].

Goguen and Meseguer in [10] presented a notion of module for a sorted theory of Horn clauses with equality. Their modules have associated with them Horn clauses, and they provided a mechanism of module importing called enriching. Their notion of importing is one of accumulation; that is, if module M_{1} imports M_{2}, the clauses associated with M_{2} are also associated with M_{1}. Hence, modules are not imported for simply private use. Instead, modules form a use hierarchy which shows which modules are parts of other modules. With the accumulation approach, searching for a clause whose head matches a given atomic goal requires searching through all modules which are reachable in the use hierarchy from the current module no matter how remote such modules are. Using the more restrictive approach of this paper, only those explicitly imported modules are searched. Such a search can, of course, be more constrained.

Several researchers have investigated extensions of positive Horn theories in an entirely classical logic setting. The resulting operational and model-theoretic semantics are quite different from those investigated here. For example, the HORNLOG system of Gallier and Raatz [8] permits programs to be general Horn clauses; that is, programs can contain any number of negative clauses. As such, the database constraints described in Section 7 can be written directly as negative Horn clauses. Queries asked of such a system, however, may have “disjunctive” answer substitutions. For example, if HORNLOG were given the query

∼(p(a) ∧ p(b)) ⊃ ∃x ∼p(x),

it would succeed and provide the disjunctive answer substitution claiming that x would get either a or b. The corresponding query in the logic presented here would be written as

(p(a) ∧ p(b) ⊃ ⊥) ⊃ ∃x (p(x) ⊃ ⊥)

and would not be provable because there is no “simple” answer substitution. Fitting in [6] used classical logic to investigate an extension of Horn clauses which contained A Logical Analysis of Modules 10. Acknowledgments

negations within the body of clauses. His model theory for such clauses used partial models (also attributed to Kripke). The operator used in building partial models as fixed points, however, is not continuous. Weakening logic from classical to intuitionistic is one way to preserve both simple answer substitutions and continuous fixed point operators in extensions to Horn clause logic.

10. Acknowledgments We are grateful to Greg Hager, Thorne McCarty, Gopalan Nadathur and Wayne

Snyder for valuable comments on a previous version of this paper. John Hannan and a reviewer provided valuable comments on this version of the paper.

11. References

1. Apt, K. R. and van Emden, M. H., Contributions to the Theory of Logic Programming JACM, 29:841 – 862 (1982).

2. Bowen, K. A. and Kowalski, R. A., Amalgamating language and metalanguage in logic programming, in: K. L. Clark and S. A. Tarnund (eds.), Logic Programming, Academic Press, 1982, 153 – 172.

3. Bowen, K. A. and Weinberg, T., A Meta-Level Extension of Prolog, 1985 Symposium on Logic Programming, Boston, 48 – 53.

4. Chomicki, Jan and Minsky, Naftaly H., Towards a programming environment for large Prolog programs, 1985 Symposium on Logic Programming, Boston, 230 – 241.

5. Fitting, M. C., Intuitionistic Logic Model Theory and Forcing, North-Holland Pub. Co., 1969.

6. Fitting, M. C., A Kripke-Kleene Semantics for Logic Programming, Journal of Logic Programming, 2:295 – 312 (1985).

7. Gabbay, D. M. and Reyle, U., N-Prolog: An Extension of Prolog with Hypothetical Implications. I, Journal of Logic Programming 1:319 – 355 (1984).

8. Gallier, J. H., and Raatz, S., HORNLOG: A Graph-Based Interpreter for General Horn Clauses, Journal of Logic Programming 4:119 – 155 (1987).

9. Gentzen, G., Investigations into Logical Deductions, in: M. E. Szabo (ed.), The Collected Papers of Gerhard Gentzen, North-Holland Publishing Co., Amsterdam, 1969, 68 – 131.

10. Goguen, J. A. and Meseguer, J., EQLOG: Equality, Types and Generic Modules for Logic Programming, Journal of Logic Programming 1:179 – 209 (1984).

11. McCarty, L. T., Fixed Point Semantics and Tableau Proof Procedures for a Clausal Intuitionistic Logic, Technical Report LRP-TR-18, Rutgers University, 1986.

A Logical Analysis of Modules 11. References

12. Miller, D., A Theory of Modules for Logic Programming, IEEE Symposium on Logic Programming, Salt Lake City, September 1986, 106 – 115.

13. Miller, D., Hereditary Harrop Formula and Logic Programming, VIII International Congress of Logic, Methodology, and Philosophy of Science, Moscow, August 1987.

14. Miller, D. and Nadathur, G., Higher-Order Logic Programming, 1986 International Conference on Logic Programming, London, 448 – 462.

15. Miller, D., Nadathur, G., and Scedrov, A., Hereditary Harrop Formulas and Uniform Proof Systems, Second Annual Symposium of Logic in Computer Science, Cornell University, June 1987, 98 – 105.

16. Nait Abdallah, M. A., Procedures in Horn-Clause Programming, 1986 International Conference on Logic Programming, London, 433 – 447.

17. O’Keefe, R., Towards an Algebra for Constructing Logic Programs, 1985 Symposium on Logic Programming, Boston, 152 – 160.

18. Prawitz, D., Natural Deduction, Almqvist & Wiksell, Uppsala, 1965.

19. Smorynski, C., Applications of Kripke models, Chapter V in [21].

20. Sterling, L., Shapiro, E., The Art of Prolog, MIT Press, 1986.

21. Troelstra, A. S., Metamathematical investigations of intuitionistic arithmetic and analysis, Lecture Notes in Mathematics 344, Springer-Verlag, Berlin, 1973.

22. Warren, D. S., Database Updates in Prolog, Proceedings of the International Conference on Fifth Generation Computer Systems, 1984, 244 – 253.