Chapter 1

Clause Complementation

1.1 Introduction

Consider the following judgment to check whether a lambda terms in linear, if every functional subterm uses each of its arguments exactly once:

e_{1} linear e_{2} linear
linear·
(e_{1} e_{2}) linear

λx . e linear in x  \frac{u}{x linear} ; ⋮ ; e linear

linearλ^{x,u}
λx . e linear

\frac{λ}{λx . x linear in x}

λx . e linear in x
λ^{y}
λx . λy . e linear
λx . e_{1} linear in x
1·
λx . (e_{1} e_{2}) linear in x

λx . e_{2} linear in x
2·
λx . (e_{1} e_{2}) linear in x

Intuitively, we check for linearity of a function making sure that the latter is linear in its first argument (judgment λx . e linear in x) and then recurring on the rest of the expression. Note the rule ‘ linearλ^{x,u}’ is hypothetical in u and parametric in x; rule λ^{y} is instead only parametric in x.

Frameworks based on hhf provide an ideal syntax to represent these judgments; namely, via the usual encoding introduced in Example ??:

linlam : linear(lam λx . E x)

← linx(lam λx . E x)

← (∀x:exp. linear(x) → linear(E x)).
linapp : linear(app E_{1} E_{2})
← linear(E_{1})
← linear(E_{2}).
linxx : linx(λx . x).
linxap1 : linx(λx . app (E_{1} x) E_{2})
← linx(λx . E_{1} x).
linxap2 : linx(λx . app E_{1} (E_{2} x))
← linx(λx . E_{2} x).
linxlm : linx(λx . lam(λy . E x y))
← (∀y:exp. linx(λx . E x y)).

The judgment and its implementation is clearly a decision procedure. It does make sense to ask ourselves what is its complement. An expression is not linear if there is some function which either does not use its argument or uses them more than once. We first observe that, since linear is a relation, defined via exhaustive and exclusive patterns, term complementation does not play a role. Then, the complement of linapp does not pose any problem, as it is a Horn clause: an application in not linear if either the first element or the second in not linear.

¬linapp : ¬linear(app E_{1} E_{2})
← ¬linear(E_{1}) ∨ ¬linear(E_{2}).

A lambda expression in not linear in two cases: first it is not linear in its first argument:

¬linlam1 : ¬linear(lam(λx . E x))
← ¬linx(lam(λx . E x)).

Secondly, if its body is not linear. Now, this poses a new problem, as we have to negate a hypothetical and parametric clause. Suppose we are given, in the empty context a goal linear(lam(λx . lam(λy . x))), which is unprovable, since the second lambda term is not linear in y; the proof tree yields the failure leaf linx(λx . y), for a new parameter y, in the context y:exp; linear(y). Our guiding intuition is that we want to mimic a failure derivation so as to provide a successful derivation from the negative definition, i.e. a proof of ¬linx(λx . y) from y:exp; linear(y); this shows one prominent feature of complementation of an HHF formula: negation ‘skips’ over ∀ and →, since it need to mirror failure from assumptions.

Let us turn to complementing linear in x. A first point to note in that, by encoding an expression ‘e’ with a pattern variable, we must make sure that in clause linxap1,linxap2 x, does not occur in the argument which is not checked.

We thus embed the clause in the strict λ-calculus and ‘E’ in the simple term ‘E x^{0}’. For the sake of readability we do this only for the two aforementioned clause and we also hide ()^{u} annotations.

linxap1 : linx(λx . app (E_{1} x) (E_{2} x^{0}))
← linx(λx . E_{1} x).
linxap2 : linx(λx . app (E_{1} x^{0}) (E_{2} x))
← linx(λx . E_{2} x).

Via term complementation in the strict λ-calculus we obtain, among others:

¬linx1 : ¬linx(λx . app (E_{1} x) (E_{2} x^{1})).
¬linx2 : ¬linx(λx . app (E_{1} x^{1}) (E_{2} x)).

Moreover, as in the case of top-level application, the complement of linxapi hold if the body does not hold:

¬linxap1 : ¬linx(λx . app (E_{1} x) (E_{2} x^{0}))
← ¬linx(λx . E_{1} x)
¬linxap2 : ¬linx(λx . app (E_{1} x^{0}) (E_{2} x))
← ¬linx(λx . E_{2} x).

Now, let us examine clause linxlm and let us reconsider the failure leaf linx(λx . y) form the context y:exp; linear(y). In a first attempt, according to the idea above, let us consider what the complement would be:

¬^{?} linxlm : ¬linx(λx . lam(λy . E x y))
← (∀y:exp. ¬linx(λx . E x y).

However, there is no way to obtain a proof of ¬linx(λx . y) from the current context. Indeed, the linxlm clause does not carry to enough information by itself so that its complement can mimic the failure proof. In a sense that we will make precise, the clause, and in turn its predicate definition is not assumptioncomplete: once it has introduced a new parameter, the clause only specifies how to use it in a positive context. It is up to us to synthesize its dynamic definition, in this case exactly ¬linx(λx . y). More generally, it is a characteristic of HHF that the negation of a clause is not enough to determine the behavior of a program under complementation. We will have to insert via a source-to-source transformation additional structure in a predicate definition in order to completely determine the provability and failure of goals which mention parameters. By observing the structure of all possible assumption that a predicate definition can make, we will augment those assumptions with their negative definition. In particular, we first augment the clause linxlm:

aug_{D}(linxlm) : linx(λx . lam(λy . E x y))

← (∀y:exp. ¬linx(λx . y) → linx(λx . E x y)). so that, by complementation, we obtain

¬aug_{D}(linxlm) : ¬linx(λx . lam(λy . E x y))

← (∀y:exp. ¬linx(λx . y) → ¬linx(λx . E x y)).

In summary the negative program is:

¬linapp : ¬linear(app E_{1} E_{2})
← ¬linear(E_{1}) ∨ ¬linear(E_{2}).
¬linlam1 : ¬linear(lam(λx . E x))
← ¬linx(lam λx . E x) ∨
(∀x:exp. linear(x) → ¬linear(E x)).

¬linx1 : ¬linx(λx . app (E_{1} x) (E_{2} x^{1})).
¬linx2 : ¬linx(λx . app (E_{1} x^{1}) (E_{2} x)).
¬linxap1 : ¬linx(λx . app (E_{1} x) (E_{2} x^{0}))
← ¬linx(λx . E_{1} x).
¬linxap2 : ¬linx(λx . app (E_{1} x^{0}) (E_{2} x))
← ¬linx(λx . E_{2} x).
¬linxlm : ¬linx(λx . lam(λy . E x y))
← (∀y:exp. ¬linx(λx . y) → ¬linx(λx . E x y)).

While it is not impossible to manually come up with this program by writing a definition for strict and vacuous and then merging them in the correct fashion, it would be better to have this dome automatically, especially considering changes or extensions of the original program.

Unfortunately the procedure we have outlined is not possible in general. Consider a clause encoding the introduction rule for implication in natural deduction, which can be used to check whether an implicational formula trivially holds:

Example 1.1

Σ : form:type, imp:form → form → form, a:form, b:form, c:form
impi : nd(A imp B) ← (nd(A) → nd(B)).

Following our earlier remark its complement would be:

¬impi1 : ¬nd(a)
¬impi2 : ¬nd(b)
¬impi3 : ¬nd(c)
¬^{?} impi : ¬nd(A imp B) ← (nd(A) → ¬nd(B)).

Apparently this specification is incorrect since both nd(a imp a) and ¬nd(a imp a) are derivable from the empty context. We can isolate one major problem: in clause impi the assumption nd(A) which is dynamically added to the (static) definition of the nd predicate overlaps with the head of the clause. A symmetrical problem can occur when dynamic and static cause do differ but their complements do not. Suppose we introduce a predicate which checks is a number is even and non zero as follows:

e : ev(s(s(N))) ← (ev(0) → ev(N)).

Again, our naive algorithm would incorrectly yield:

¬e1 : ¬ev(0).
¬e2 : ¬ev(s(0)).
¬^{?} e : ¬ev(s(s(N))) ← (¬ev(s(0)) → ¬ev(N)).

Thus both ev(s(s(0))) and ¬ev(s(s(0))) are incorrectly provable. The problem here is the overlapping between the of assumption ev(0) and the complement of the head of the e clause.

We have thus isolated two main issues:

1. Exhaustivity: we need to enrich clauses so that every (ground) goal or its negation is provable.

2. Exclusivity: we need to isolate a significant fragment where it is not the case that both a goal and its negation are provable.

We will describe in Section 1.9 a procedure that we call augmentation, which, by enriching the program with the complement of assumptions will, will achieve exhaustivity (1.11); moreover, we will achieve exclusivity with the restriction to complementable programs, formally introduced in Figure 1.7. To anticipate the idea, a clause is complementable if every assumption is parametric in some eigenvariable. We will try to motivate in Section 1.3 why this fragment is adequate in the practice of logical frameworks. Section 1.4 reviews some related work in the area of NF and embedded implication.

1.2 Background

Traditionally, a completion construction for the NF rule is an extension of a program, say E(P) such that, in a logic L equipped with a provability and finite failure relation, say ⊢_{L} and ⊣ ⊢_{L} and a negation sign ¬, for any given goal G and a consequence relation ⊧_{L}, it holds:

1. If ⊢_{L} G, then E(P) ⊧_{L} G.

2. If ⊣ ⊢_{L} G, then E(P) ⊧_{L} ¬G .

Many such constructions have been proposed for Horn logic, starting from the Closed World Assumption (CWA) [Rei78]. The Clark completion [Cla78] is perhaps the most successful proof-theoretic and finitary explanation of NF : the main idea is that clauses in a predicate definition should be seen as an iff-definition, thus enforcing the minimality condition of its inductive definition; this would correspond, in model-theoretic terms, to the existence of a least intended model. The if-part states the condition to belong to the inductive definition, while the only-if part excludes everything else, thus providing a computable approximation to the CWA. This is well understood and agreed as far as Horn logic is concerned and confirmed by the completeness of finite failure w.r.t. the completion [Apt90].

As observed first by Gabbay [Gab85], the positive logic of embedded implication is not classical but intuitionistic (actually minimal). When coupled with negation as failure in all its generality, its meta-logic fails to have some straightforward logic properties, as detailed in Section 1.4. The key difference lies in the constructive interpretation of implication and its delicate interplay with negation. While a completion construction is possible, it is not equivalent to the adjoining of the only-if part of the program. This is intrinsically due to the operational semantic of failure: a goal D → G fails iff from the (scoped) assumption D we have that G fails. Let us try to mirror this with a logical connective”

¬(D → G) =^{?} D → ¬G

Similarly for parametric judgments:

¬(∀x:A. G) =^{?} ∀x:A. ¬G

No standard logic of negation satisfies the above rules. In particular, it is erroneous to formulate Clark’s completion using Nelson’s strong negation [Nel49], which is currently held as the meta-logic of negation elimination in the Horn setting [GL90, Pea90]. Indeed, strong negation brings too much duality to intuitionistic logic as it is pushed in through connectives and quantifiers; in particular if ∼ denotes strong negation the following holds:

∼ (D → G) ↔ D∧ ∼ G
∼ (∀x:A. G) ↔ ∃x:A. ∼ G

Strong negation may be “the logic of information structures” [Wan93], as far as Horn logic is concerned, but it is definitely not the meta-logic of negation elimination in logical frameworks based on hhf. It is not simply a question to endow intuitionism of a semi-classical notion of negation, while preserving the disjunction and existential property. The hard point is not negation in itself, but its interaction with a more operational Brower-Heyting-Kolmogorov interpretation of implication.

Example 1.2 Consider the program consisting only of the clause a ← (b → c); the standard completion would be

a ↔ (b → c) ∧ ¬b ∧ ¬c Now, ′a′ fails and hence ′¬a′ should follow from the iff-completion: still ′a′ intuitionisticallly (yet not minimally) follows, while ′¬a′ is logically independent exactly due to the failure of Equation (1.1).

We explore in Section 1.4 how this issue has been investigated in the literature. This is relevant to our enterprise as:

• In the Horn setting, the iff-completion has been the preferred way to logically motivate the transformational approach to negation, as detailed in Chapter ??.

• In [GO98] the authors persuasively argue that the unrestricted addition of NF to N-Prolog requires the switch to a (three-valued) modal logic.

Since we need to express the negation of a predicate in the same language where the predicate is formulated, we choose to restrict the set of programs we deem complementable in a novel and extensive way. This will help to close the gap between the two poles usually associated to classic and intuitionistic logic programming, i.e. the closed versus open world assumption. We will define a class of programs which extend the current database in a specific regular way, by ensuring that static and dynamic clauses never overlap. This property extends w.r.t. the complement program and thus has the side effect of guaranteeing the consistency of the completion. We argue next (Section ??) that this class of programs is just what the doctor ordered for logical frameworks.

1.3 Motivation

Embedded implication in intuitionistic logic programming has been successfully used in various areas of logic programming; we can roughly divide those into:

• Meta-programming, namely specifying and implementing (the meta-theory of) deductive systems.

• Hypothetical reasoning in databases [GR84, BMV89, Bon94] or simulating imperative-style programming [BM90].

• Incorporating modules and local predicate definitions [Mil89, GMR92, KNW93] and state encapsulation in object-oriented programming [?].

We now try to motivate why the restriction of complementation to parametric implication (formally defined in Section 1.8) is pragmatically adequate for our intended application.

While implementing deductive systems embedded implication is usually coupled with higher-order abstract syntax to represent scoping constructs: the latter are typically used to traverse operators like abstractions, quantification and, more pervasively, to represent rules with hypothetical premises. In this application implications are typically ‘covered’ by an intensional universal quantifier which express the parametricity of the assumption. Dozens of examples can be found for instance in [Pfe92]. One counter-example I am aware of is when using a logic framework to encode derivability in an object logic: here meta-logic contexts are used to manage object logic hypotheses, as in Example 1.1. We feel that this case in not typical; first of all it is questionable (and out of the scope of a logical framework) to complement recursive enumerable predicates such as general provability. Even if we limit ourselves to decision procedures as propositional logic, we are in a sense asking for a self-referential use of implication as we wish to represent implications in the object logic with the same in the meta-logic. In this case, though we have no formal proof of this, we think we have to use ad hoc techniques such as explicit management of hypotheses say as lists; a similar approach is taken in [MM97].

Modules are usually closed assumptions and I doubt negation is useful at this level. Local definitions, as an auxiliary reverse3 procedure hidden inside the naive reverse procedure are typical only in higher-order logic programming languages as λProlog, and require full predicate quantification. We conjecture that some of those programs can be complemented if there is no overlap between static and dynamic clauses. As far as object-oriented programming is concerned, we have not investigated the issue so far.

The possibility to simulate the availability of global variables in logic programming has been advocated [GO98] as the main motivation of the intertwined and unrestricted use of negation and embedded implication. We contend that sometimes that can be resolved with a refined notion of context as the one available in linear logic programming: this has also the side-effect of by-passing the issue of non-stratification.

We now exemplify how to eliminate negation from non-stratified N-Prolog programs. We cannot say at the moment whether this transformation can be generalized and eventually mechanized.

The following example (taken from [GO98]) is a non-stratified program to compute the parity of a relation encoded as n entries of the form r(X), where ‘\+’ denotes negation-as-failure:

Example 1.3 (Parity)

\begin{matrix}even ← \ + odd. \\ odd ← r(X), \ + mark(X), (mark(X) → even). \end{matrix}

We can write a Lolli program [HM94] based on the same algorithm, where the linear context contains the entries of the relation and the initial token empty; let −∘ and ⊗ denote linear implication and conjunction:

even ← r(X) ∧ (empty −∘ full ⊗ odd).
even ← full.
odd ← r(X) ∧ (full −∘ empty ⊗ even).
odd ← empty.

1.4 Related Work

Recently there has been some interest in combining NF with what is known as intuitionistic logic programming. The underlying languages, with the exception of [Har93], are either versions of N-Prolog or clausal intuitionistic logic. Due to the inherently difficulty with universal quantification mentioned in ??, the treatment is deprived of parametric goals. The emphasis is not on the transformational approach but to combine the non-monotonic nature of NF with the capability of embedded implication to dynamically update the current program. We will not detail here the proposed semantics (stable models [Dun92], monotonic Kripke-like models [Har89], non-monotonic perfect [BM90] or three-valued [GO98] models).

Gabbay [Gab85] pointed out that NF coupled to embedded implication seems to lead to curious paradoxes, at the point of making the whole enterprise not logically sound. This problem arises already when dealing with (propositional) normal clauses. They can be summarized as follows (taken from [NL92]).

1. Failure of transitivity, or, in other words, non-eliminability of the cut rule.

Let P be:

\begin{matrix}a ← b ∧ \ + c \\ b ← c \end{matrix}

Now, P ⊢ c → b and P ⊢ b → a, as c is undefined, but c → a is not provable from P.

2. Failure of weakening. Let P be:

b ← \ + a

Then P ⊢ b but a → b is not provable form P.

3. “Pathology of negative information”, i.e. P ⊢ \ + (A → B) iff P ⊢ A → \ + B.

There are several solutions to this riddle:

• A modal completion [GO98].

• A syntactic distinction between implications [BM90].

• A syntactic distinction between predicates [Har93].

We detail the latter next, but let us state, for the record, our position:

1. Provability must take into account the context where the query is attempted: in case 1. the first query is not allowed, since b is a predicate which must be called from an empty context.

2. Similarly, a → b is not a legitimate query as b must be queried in the empty context.

3. This is indeed the operational semantics of failure of hypothetical judgments; the issue is giving a logical justification of that and the challenge is to give it without changing the logic underneath.

1.4.1 NF in Clausal Intuitionistic Logic

We can regard Clausal Intuitionistic Logic as a close cousin of uniform proofs independently developed by McCarty in the late eighties [McC88a, McC88b]. NF in this setting has been investigated in Bonner’s thesis [Bon91] and is summarized in [Bon94]. The framework in [BM90] is hypothetical datalog (with possibly infinite constants) and embedded implications. They assume a notion of negation-stratification and develop an awkward proof-theory parameterized by strata; a non-monotonic preferred Kripke model theory is presented and adequacy is demonstrated. They offer the following solution to the aforementioned paradoxes: the implication sign is really two distinct connectives, one for clauses and one for goals. Clause implication is interpreted classically and it is transitive, while goal implication is not and must be interpreted non-monotonically. Indeed the latter has a modal semantic which takes into account the extension of a context as a shift in worlds (in the Kripke sense). While we favor a syntactic distinction between goals and clauses, the uniform proof approach views implication as logical (intuitionistic) implication whose different behavior is simply dictated by its introduction and elimination rule. Moreover we do not aim to deal with arbitrary extensions. We have hinted in the previous section how linear logic programming can address examples in this paper which are outside the fragment we are able to treat.

1.4.2 NF and N-Prolog

This approach has been investigated first at the propositional level in [NL92] and then for first-order N-Prolog in [GO98]:

“In order to understand N-Prolog computations with NF , we must adopt a dynamic view of success and failure […] we cannot determine what goals succeeds or fail from a program unless we determine what goal succeeds or fail from arbitrary^{1} extension of the program”

[NL92] pp. 258

The main idea is again that a computation of an implicational goal D → G from P entails a shift to another world where P ∪ D holds. The authors propose a completion construction as an explanation of negation-as-failure. The completion is formulated as an infinite theory such that comp_{n}(P) is used to evaluate a goal G roughly if we need n extensions of the program to compute G: for example for a clause a ← (b → c) then a is provable iff comp(P ∪ b) entails c and a is false iff comp(P ∪ b) entails ¬c. Note that comp(P ∪ b) is different from comp(P) ∪ b or comp(P) ∪ comp(b). Moreover, due to the possible nonmonotonicity of arbitrary extensions comp(P) and comp(P ∪ b) may be jointly inconsistent: the modality represents then the shift of context. The completion construction does not seem to generalize immediately to universally quantified goals. The right kind of logic turns out to be a three-valued version of K4. The authors prove soundness and completeness of ESLDNF derivability w.r.t. a Kripke-Kleene fixpoint construction for a notion of non-floundering programs. The three-valued approach avoids the restriction to stratified programs.

1Emphasis is mine.

Draft of February 28, 2000

1.4.3 NF in first-order Uniform Proofs

Harland’s thesis [Har91] is an in-depth analysis of Uniform Proofs and NF at the first-order level. Unfortunately, his approach, though sound, is not adequate to our purposes, as we shall argue next. Harland inherits the traditional ‘boolean’ attitude w.r.t. the closed world assumption: predicates are either completely defined (CWA), as in the append program, or incomplete (OWA); while this distinction, he maintains, is essentially semantic and therefore enforced by user declarations, the latter coincide with the programs where temporary assumptions are made, i.e. clauses with embedded implications. Thus NF would make sense only for the former, since how, will you apply the CWA to something that is by definition incomplete? Therefore those programs would require some form of real (say minimal) negation, much as in [Mil89, Mom92]. Technically, this is achieved by distinguishing, for all predicates occurring in the signature, those which appears negatively versus positively in the body of clauses. The two sets are required to be disjoint. This of course simplify the later development, but, unfortunately, if a predicate which appears negatively, i.e. it is assumed, cannot occur positively, then it will never be used in the derivation. Its assumption is totally irrelevant to the computation and may be discarded from the program. This fragment therefore collapses to normal programs with extensional quantification. While it is possible to enforce differently the distinction between complete and incomplete predicates, we are indeed interested to apply negation to incomplete predicates, although in a restricted fashion.

Then Harland shows how to formulate the completion as an object fohh formulae so as to simulate NF as derivability in the uniform proof system. The executable completion is formulated through contraposition. Programs are assumed to be locally stratified, hence the completion is consistent. Thus Harland identifies the completed programs with its iff-completion, though he correctly has ¬(D → G) = D → ¬(G). This operational interpretation of the augment instruction w.r.t. negation is nevertheless inconsistent with its formulation in the completion, where negation is interpreted classically insofar as the negative completion of Q ← G is seen as ¬(Q ∧ ¬G); again this holds only because NF cannot be applied to incomplete predicates. The classical attitude carries over to universal quantification, which is only allowed to be extensional. Harland so does not stress the intrinsic connection between implication and parametric universal quantification. Extensionality is achieved through covering as in [MMP88], though the role of the DCA (Domain Closure Axiom) is not made explicit. Therefore Harland is not able to correlate extensional uniform proofs with intuitionistic provability plus DCA. This is not surprising since its partition between complete and incomplete predicates restricts the AUGMENT rule so that its operational provability relations are not conservative extensions of standard uniform provability: this makes the usual proof-theoretic adequacy impossible. Moreover no operational semantic for coverings is described: not only the role of free variables introduced by coverings is unclear, but the extensional rules are totally non-deterministic w.r.t. the choice of the correct covering.

An equality/inequality solver on the Herbrand universe is described and used to solve inequalities stemming from the completed definitions: this algorithm is different from the traditional uncover algorithm as it does not return the most general solution but a possibly infinite enumeration of the latter; this permits not to left linearize the program.

1.4.4 PID

Partial Inductive Definitions ([Hal91]) are a generalization of inductive definitions [Acz77] to definiens containing implications and in a finitary version ([Eri93]) parametric quantification: they also incorporate a proof-theoretical notion of closure somehow as in the CWA, but brought upon by the principle of definitional reflection. In a logical setting, following [SH93], we take an intuitionistic sequent calculus parameterized by a set of definitions, i.e. a finite set of clauses b ⇐ G, where b ranges over atomic predicates possibly with free variables. For a definition D, we call D(a) = {σG | b ⇐ G ∈ D, a = σb}. In the spirit of the “clauses-as-rules” paradigm [HSH90, HSH91] we add for every defined atom a, the rules

\begin{aligned}Γ ⊢ G G ∈ D(a) \\ & D − R \\ Γ ⊢ a \end{aligned} \begin{aligned}\{σΓ, σG ⊢ A : σ = mgu(a, b), b ⇐ G ∈ D\} \\ & D − L \\ Γ, a ⊢ A \end{aligned}

Call this DR(D), for a given set of definitions D. The first rule corresponds to backchaining on the definitional clauses, while the second, in its ω-version, reflect the closure clause of (partial) inductive definitions. They can be seen as right and left introduction rules for the atomic proposition a: This feature is used in the programming language GCLA [MAK91] which allows both functional and logic programming style. Search is conducted on sequents Γ ⊢ G and it is clearly not amenable of a uniform proof approach, since focusing is impossible as at any time each of the assumption in the antecedent may be expanded via D − L. Indeed, without mentioning the issue of contraction, control in this setting has proven to be a major problem and this has lead to GCLA II, which is a middle ground between a logic programming language and a tactic theorem prover [Kre92].

One basic problem is the failure of global cut-elimination: as discussed in [SH93], in order to reduce an atomic cut formula through the D − L/D − R reduction, we may generate a cut with a more complex definiens formula. Definitions are called total if they enjoy cut-elimination, otherwise they are partial. Classes of total definitions include:

• Implication-free programs.

• Contraction-free logics.

• Stratified program w.r.t. negation.

• Stratified program w.r.t. implication [MM97].

In the latter case, predicates are assigned levels: the latter are then extended to formulae, so as to forbid recursion through negative occurrences; the level of an implication is essentially the order of its type: definitions are allowed only if the level of the heads is strictly greater then the level of the body: for instance a ⇐ b → a is allowed while a ⇐ a → b is not. This excludes every left-recursive definition.

Definitional reflection brings in a proof-theoretic notion of negation. Intuitively, D − L works as the only-if clause of the completion: a proof of ⊢ ¬a is a proof of a ⊢ ⊥. This has been formalized by Schroeder-Heister who has proven [SH93] the equivalence between comp(P) and DR(P) ∪ (x = x ⇐ ⊤), where the latter clause, thanks to definitional reflection, suffices to define free equality. This result holds for any kind of definition and does not depend on cut-elimination. This has been hailed by the GCLA group as a major benefit of allowing definitional reflection. This claim has some validity as far as normal stratified programs and ground goals are concerned: indeed they may yield only sequents such that if the antecedent is non-empty, it must be atomic and the consequent is ⊥: then D − L must be used to introduce a definiens from a lower stratum. As mentioned above, search is here cut-free. The equivalence with the completion holds irrespectively of the presence of local variables. In this remark, then this approach would seem to have an edge on the transformational one since it does not need extensional quantification.

Example 1.4 Consider a graph edge(a, b), edge(b, c): the deduction of path(b, a) ⊢ ⊥ leads to the conjunctive goals {(edge(b, a) ⊢ ⊥), (edge(b, Z)∧path(Z, a) ⊢ ⊥}, where Z is a local logic variable; then there is a computation which reduces to ⊥, Γ ⊢ ⊥.

On the other hand the issue with negative goals arises when concerned with open queries. When logic variables are allowed PID’s give the usual unsound reading to existential queries and one is faced again with the question of failure substitutions. For example the query ⊢ ∃x¬even(x) yields even(X) ⊢ ⊥; the rule D − L will loop, being unable to compute to what amounts, in our terms, to Not(0) ∩ Not(s(s(Y))).

I am not aware of any implementation of the ω-rule for the purpose of enhancing a logic language with negation. As a matter of fact, the rule of definitional reflection used in GCLA is the weaker ‘logical’ version [MAK91] which does not imply in general the completion.

Notwithstanding the similarity, PID’s give a striking different operational semantics to hhf. Consider for example the definition a ⇐ b → c: then the sequent ⊢ ¬a has no cut-free proofs, while ⊢ a is provable against the operational intuition of hhf:

\frac{D − L}{b ⊢ c} ; → −R ; ⊢ b → c

D − R
⊢ a

Here, since b has no definition, it is assumed to be false and hence entails anything. This means that D − L is not conservative w.r.t. the positive fragment, i.e. the former rule may be used in proving positive atoms. In the complementation approach instead, positive and negative fragments are disjoint and exclusive. This is no surprising since, as mentioned above, the equivalence with the iff completion induces an operational semantics of failure which is distinct from the one typical of hhf. Moreover definitional reflection does not match well with parametric judgments:

[Elaborate ]

1.5 The Logic

We will use the following slightly unusual source language: let M⃗, N⃗ be sequences of simple terms:

Atoms Q ::= q M⃗ | ¬q M⃗
Goals G ::= Q | ⊤ |⊥| M⃗ =^{·} N⃗ | M⃗ ≠^{·} N⃗ |
G_{1} ∧ G_{2} | G_{1} ∨ G_{2} | D → G | ∀x:A. G | ∃x:A. G
Clauses D ::= ⊤ |⊥| Q | D ← G | D_{1} ∧ D_{2} | D_{1} ∨ D_{2} | ∀x:A. D

Differently form standard presentation of HHF, we allow disjunction between clauses, equality and inequality. While disjunction among clauses will be eliminated, (in)equalities containing parameters will not. This means that in typetheoretic languages such as Twelf they need to be viewed as types inhabited by appropriate proof terms. However, since (in)equalities will be treated exclusively as constraints, we will not need a complicate treatment as in Martin-Löf’s type theory. The tokens ⊤ and ⊥ may be decorated with a predicate symbol. Finally, we remark that ‘¬’ is not a connective, but a name constructor for atomic formulae.

Parameter Contexts Γ ::= · | Γ, x:A
Assumptions D ::= ⊤ | D ∧ D

We call a pair of concrete context and assumption Γ; D, such that all parameters occurring in D are mentioned in Γ, a (run-time) context. We make the usual conventions on contexts, in particular we avoid mentioning the leading · and ⊤ elements.

Definition 1.5 (def(q, D))

def(q, ⊤) = ⊤_{q}
def(q, ⊥) = ⊥_{q}
def(q, Q ← G) = Q ← G  if Q ≡ q M⃗
def(q, Q ← G) = ⊤_{q}  otherwise
def(q, ∀x:A. D) = ∀x:A. def(q, D)
def(q, D_{1} ∧ D_{2}) = def(q, D_{1}) ∧ def(q, D_{2})
def(q, D_{1} ∨ D_{2}) = def(q, D_{1}) ∨ def(q, D_{2})

If D = P, i.e. the underlying program (seen as a conjunction of clauses), we call def(q, P) the static definition of q. If D is a conjunction of run-time assumptions, we call the latter the dynamic definition of q. As a special case, an undefined predicate q, i.e. a predicate which occurs in a body of a clause but not as a head is represented by the empty conjunction ⊤_{q}. Conversely ⊥_{q} denotes the universal definition for q. We use the notation D ∈ def(q, P ∧ D) to indicate that D is a top-level conjunct in the definition of q.

We now introduce the uniform proofs judgments for provability and denial in Figure 1.1 and for immediate implication and denial in Figure 1.2. Due to the presence of ‘∨′ as a clause constructor, uniform proofs are not complete w.r.t. intuitionistic logic. We will remedy this situation in Section 1.12.1. The rules are depicted (when possible) in two columns where every row displays a positive rule and its negative counterpart. We remark that the systems for denial will not be needed in the proof of exclusivity (Theorem 1.27).

Γ; D ⊢_{P} G  Program P and assumption D uniformly entail G.
Γ; D ⊬_{P} G  Program P and assumption D uniformly deny G.
Γ; D ⊢_{P} D>>Q Clause D from def(q, P ∧ D) immediately entails atom Q.
Γ; D ⊬_{P} D>>Q Clause D from def(q, P ∧ D) immediately denies atom Q.

We briefly comment on the rules: the (in)equalities rules simply mirror the object logic symbols =^{·}, ≠^{·} in meta-level (in)equality. Note that ≯>∀ and ⊬ ∃ are infinitary rules, due to the meta-linguistic extensional universal quantification on all terms. Rule ≯>∀ must be read as: for every well-typed term n in parameter context Γ, ∀x: A. D immediately denies Q if so does [n/x]D. Analogously for ⊬ ∃. Rules ⊢ ∀, ⊬ ∀ are instead parametric in the new eigenvariable, say y; the ()^{y} superscript reminds us of the parameter condition on y, e.g. that y does not occur free in Γ; D nor in G. We will use this notation in any other parametric rule.

Differently from the latter, we will also use global eigenvariables, say u (see for example rules ⟹^{D} ∀ and ⟹^{G} ∃ in Figure 1.3); this expresses the fact that in those rules the relation holds for any term and are therefore synonymous to logic variables. We will pervasively utilize this notation and to avoid notational clutter, we shall not keep an explicit record, but we agree to implicitly gather them in a pool Φ, which we can access when needed.

The denial rules for implication and universal quantification reflect the operation semantics of unprovability that we have discussed earlier. For the sake of conciseness we will often use in this thesis the following rule schema, where J (X, R) is a judgment involving a token X ranging over a set T and a relation R:

\begin{aligned}X ∈ T \\ & R X \\ J (X, R) \end{aligned}

1.5.1 Substitutions

Since we have introduced meta-level extensional quantification we will have to introduce valid substitutions. Soundness requires the latter not only to be well-typed, but also to correctly deal with quantifier alternations, in so that substitution terms for essentially existential variables must respect the eigenvariable restriction brought in by parametric rules. We do not develop the usual theory of well-typed substitutions; we simply assume that t can be given the type associated to x.

Substitutions σ ::= ϵ | σ, t/x

The judgment Γ ⊢ σ formalizes that σ is a valid substitution w.r.t. Γ, where

1.5. THE LOGIC  17
\frac{⊢ ⊤}{Γ; D ⊢_{P} ⊤}  \frac{⊬_{⊥}}{Γ; D ⊬_{P}⊥}
\begin{matrix}M⃗ = N⃗ \\ ⊢ & =^{·} \\ Γ; D ⊢_{P} M⃗ =^{·} N⃗ \end{matrix}  \begin{matrix}M⃗ ≠ N⃗ \\ ⊬ & =^{·} \\ Γ; D ⊬_{P} M⃗ =^{·} N⃗ \end{matrix}
\begin{aligned}M⃗ ≠ N⃗ \\ & ⊢≠^{·} \\ Γ; D ⊢_{P} M⃗ ≠^{·} N⃗ \end{aligned}  \begin{aligned}M⃗ = N⃗ \\ & ⊬≠^{·} \\ Γ; D ⊬_{P} M⃗ ≠^{·} N⃗ \end{aligned}
\begin{aligned}Γ; D ⊢_{P} G_{1} Γ; D ⊢_{P} G_{2} \\ & ⊢∧ \\ Γ; D ⊢_{P} G_{1} ∧ G_{2} \end{aligned} \begin{aligned}Γ; D ⊬_{P} G_{1} Γ; D ⊬_{P} G_{2} \\ & ⊬∨ \\ Γ; D ⊬_{P} G_{1} ∨ G_{2} \end{aligned}
\begin{aligned}Γ; D ⊢_{P} G_{1} \\ & ⊢ ∨_{1} \\ Γ; D ⊢_{P} G_{1} ∨ G_{2} \end{aligned}  \begin{aligned}Γ; D ⊬_{P} G_{1} \\ & ⊬ ∧_{1} \\ Γ; D ⊬_{P} G_{1} ∧ G_{2} \end{aligned}
\begin{aligned}Γ; D ⊢_{P} G_{2} \\ & ⊢ ∨_{2} \\ Γ; D ⊢_{P} G_{1} ∨ G_{2} \end{aligned}  \begin{aligned}Γ; D ⊬_{P} G_{2} \\ & ⊬ ∧_{2} \\ Γ; D ⊬_{P} G_{1} ∧ G_{2} \end{aligned}
Γ ⊢ t : A Γ; D ⊢_{P} [t/x]G

⊢ ∃ Γ; D ⊢_{P} ∃x:A. G

for all n Γ ⊢ n : A Γ; D ⊬_{P} [n/x]G

⊬ ∃

Γ; D ⊬_{P} ∃x:A. G
\begin{aligned}Γ; (D ∧ D) ⊢_{P} G \\ & ⊢ → \\ Γ; D ⊢_{P} D → G \end{aligned}  \begin{aligned}Γ; (D ∧ D) ⊬_{P} G \\ & ⊬ → \\ Γ; D ⊬_{P} D → G \end{aligned}
\begin{aligned}(Γ, y:A); D ⊢_{P} [y/x]G \\ & ⊢∀^{y} \\ Γ; D ⊢_{P} ∀x:A. G \end{aligned}  \begin{aligned}(Γ, y:A); D ⊬_{P} [y/x]G \\ & ⊬∀^{y} \\ Γ; D ⊬_{P} ∀x:A. G \end{aligned}
\begin{aligned}Γ; D ⊢_{P} def(Q, P ∧ D)>>Q \\ & ⊢ & At \\ Γ; D ⊢_{P} Q \end{aligned}  \begin{aligned}Γ; D ⊬_{P} def(Q, P ∧ D)>>Q \\ & ⊬ & At \\ Γ; D ⊬_{P} Q \end{aligned}

Figure 1.1: Provability and Denial

Draft of February 28, 2000

18  CHAPTER 1. CLAUSE COMPLEMENTATION
\frac{>> ⊥}{Γ; D ⊢_{P}⊥ >>Q}  \frac{≯>⊤}{Γ; D ⊬_{P} ⊤>>Q}

Γ ⊢ t : A Γ; D ⊢_{P} [t/x]D>>Q

>>∀

Γ; D ⊢_{P} ∀x:A. D>>Q

for all n Γ ⊢ n : A Γ; D ⊬_{P} [n/x]D>>Q

≯>∀

Γ; D ⊬_{P} ∀x:A. D>>Q

\begin{matrix}Γ; D ⊢_{P} D_{1}>>Q \\ >> & ∧_{1} \\ Γ; D ⊢_{P} D_{1} ∧ D_{2}>>Q \end{matrix}  \begin{matrix}Γ; D ⊬_{P} D_{1}>>Q \\ ≯> & ∨_{1} \\ Γ; D ⊬_{P} D_{1} ∨ D_{2}>>Q \end{matrix}
\begin{matrix}Γ; D ⊢_{P} D_{2}>>Q \\ >> & ∧_{2} \\ Γ; D ⊢_{P} D_{1} ∧ D_{2}>>Q \end{matrix}  \begin{matrix}Γ; D ⊬_{P} D_{2}>>Q \\ ≯> & ∨_{2} \\ Γ; D ⊬_{P} D_{1} ∨ D_{2}>>Q \end{matrix}

Γ; D ⊢_{P} D_{1}>>Q Γ; D ⊢_{P} D_{2}>>Q

>>∨

Γ; D ⊢_{P} D_{1} ∨ D_{2}>>Q Γ; D ⊬_{P} D_{1}>>Q Γ; D ⊬_{P} D_{2}>>Q

≯>∧

Γ; D ⊬_{P} D_{1} ∧ D_{2}>>Q

Γ; D ⊢_{P} D>>Q Γ; D ⊢_{P} G >> →

Γ; D ⊢_{P} D ← G>>Q

\begin{matrix}Γ; D ⊬_{P} D>>Q \\ ≯> & →_{1} \\ Γ; D ⊬_{P} D ← G>>Q \end{matrix}  \begin{matrix}Γ; D ⊬_{P} G \\ ≯> & →_{2} \\ Γ; D ⊬_{P} D ← G>>Q \end{matrix}

Figure 1.2: Immediate Entailment and Denial par(t) denotes the set of parameters occurring in t:

Draft of February 28, 2000

\frac{ϵ}{Γ ⊢ ϵ}  \begin{aligned}par(t) ⊆ Γ  Γ ⊢ σ \\ & σ \\ Γ ⊢ σ, t/x \end{aligned}

For σ = σ′, t/x, we say that x is defined in σ. We require all variables defined in a substitution to be distinct: we use dom(σ) for the set of variables defined in σ and cod(σ) for the variables occurring in the substituting terms. We assume them to be disjoint. Notation: [t/x]E denotes the substitution of x with t in an well-formed expression E. More in general we denote with [σ]E the application of σ to E. We will also need an operation of composition, say σ_{1} · σ_{2}, such that [σ_{1} · σ_{2}]E = [σ_{2}]([σ_{1}]E).

1.5.2 ⊤-Normalization

We show in this section how to put every program in a normalized format w.r.t. assumptions so that every goal in the scope of an universal quantifier depends on some assumption, possibly the trivial clause ⊤. This has also the effect of ‘localizing’ the trivial assumption to its atom, a property will be very useful while performing augmentation, see Section 1.9. Some caution must be exercised to discriminate whether the universal quantifier contributes or not to the provability of the goal in its scope.

We first state some basic properties of provability.

Lemma 1.6 (Weakening)

1. If Γ; D ⊢ G, then:

(a) (Γ, x:A); D ⊢ G.

(b) Γ; (D ∧ D) ⊢ G.

2. If Γ; D ⊢ D>>Q, then:

(a) (Γ, x:A); D ⊢ D>>Q.

(b) Γ; (D ∧ D′) ⊢ D>>Q.

Proof: A straightforward mutual induction on the given derivations. □

In the proof of Theorem 1.10 we will need the following form of Strengthening:

Lemma 1.7 (⊤-Strengthening)

1. If Γ; (D ∧ ⊤) ⊢ G, then Γ; D ⊢ G.

2. If Γ; (D ∧ ⊤) ⊢ D>>Q, then Γ; D ⊢ D>>Q.

Proof: By an easy mutual induction on the structure of the given derivations. □

Normalization is realized in Figure 1.3 by the two judgments D ⟹^{D} D^{⊤} and Γ; D ⊢ G ⟹^{G} G^{⊤}. The only interesting case is when we reach an atomic goal: if no parameter has been introduced, the clause does not need any normalization. Similarly if D is non-trivial. If Γ is non-empty, there is the possibility that the type of the introduced parameter is subordinate [Vir99] to the type of the atom considered. In this case there is no need for us to introduce the trivial assumption. More formally, we say that x:A is relevant to Q if head(Q) ≡ q, Σ(q) = A_{1}, …, A_{n} → prop and for some 1 ≤ i ≤ n it holds that target(A_{i}) ≡ A; we denote this with xR^{i}q. Thus we ⊤-normalize Q only when there is a parameter in the context which is relevant to Q.

Example 1.8 Consider the lambda clause in the open program:

oplam : ∀E:exp → exp. open (lam E) ←
∀x:exp. open (E x).

As x:exp is relevant to open:exp → prop , oplam ⟹^{D} oplam^{⊤}, i.e.

oplam^{⊤} : ∀E:exp → exp. open (lam E) ←
(∀x:exp. ⊤_{open} → open (E x)).

Now consider Σ = form, term:type, all:(term → form) → form, isd:form → prop and the clause:

isdall : ∀D:term → form. isd (all D) ←
∀x:term. isd (D x).

Here as term ≢ form, then x:term is not relevant to isd:form → prop and

isdall^{⊤} ⟹^{D} isdall.

We start by showing that this transformation preserves run-time provability.

Theorem 1.9 Let Γ′; D′ ⊢ G ⟹^{G} G^{⊤}, D ⟹^{D} D^{⊤}, D ⟹^{D} D^{⊤} and Γ ⊢ θ:

1. If Γ; [θ]D ⊢ [θ]G, then Γ; [θ]D^{⊤} ⊢ [θ]G^{⊤}.

2. If Γ; [θ]D ⊢ [θ]D>>[θ]Q, then Γ; [θ]D^{⊤} ⊢ [θ]D^{⊤}>>[θ]Q.

Proof: By mutual induction on the structure of the derivation of γ :: Γ; [θ]D ⊢ [θ]G and inversion on γ′ :: Γ′; D′ ⊢ G ⟹^{G} G^{⊤} together with δ :: Γ; [θ]D ⊢ [θ]D>>[θ]Q and inversion on δ′ :: D ⟹^{D} D^{⊤}. We sketch only some cases:

Case γ ends in ⊢ At and γ′ is ⟹^{G} X, (AtΓ emp): trivial.

Case γ ends in ⊢ At and γ′ ends in At rel:

X ∈ {⊤, ⊥} or (dis)eq

⟹^{G} X

Γ; D ⊢ X ⟹^{G} X

\frac{AtΓ emp}{·; ⊤ ⊢ Q ⟹^{G} Q}

D ≢ ⊤

AtD non-emp

Γ; D ⊢ Q ⟹^{G} Q

\begin{aligned}xR^{i}q \\ & AtxR^{i}q \\ (Γ, x:A); ⊤ ⊢ Q ⟹^{G} ⊤_{q} → Q \end{aligned}  \begin{aligned}x R̸^{i}q \\ & Atx R̸^{i}q \\ (Γ, x:A); ⊤ ⊢ Q ⟹^{G} Q \end{aligned}

Γ; (D ∧ D) ⊢ G ⟹^{G} G^{⊤} D ⟹^{D} D^{⊤}

⟹^{G}→

Γ; D ⊢ D → G ⟹^{G} D^{⊤} → G^{⊤}

(Γ, y:A); D ⊢ [y/x]G ⟹^{G} [y/x]G^{⊤}

⟹^{G} ∀^{y}

Γ; D ⊢ ∀x:A. G ⟹^{G} ∀x:A. G^{⊤}

Γ; D ⊢ [u/x]G ⟹^{G} [u/x]G^{⊤}

⟹^{G} ∃^{u}

Γ; D ⊢ ∃x:A. G ⟹^{G} ∃x:A. G^{⊤}

Γ; D ⊢ G_{1} ⟹^{G} G_{1}^{⊤} Γ; D ⊢ G_{2} ⟹^{G} G_{2}^{⊤}

⟹^{G} ∧

Γ; D ⊢ G_{1} ∧ G_{2} ⟹^{G} G_{1}^{⊤} ∧ G_{2}^{⊤}

Γ; D ⊢ G_{1} ⟹^{G} G_{1}^{⊤} Γ; D ⊢ G_{2} ⟹^{G} G_{2}^{⊤}

⟹^{G} ∨

Γ; D ⊢ G_{1} ∨ G_{2} ⟹^{G} G_{1}^{⊤} ∨ G_{2}^{⊤}

X ∈ {Q, ⊤, ⊥}

⟹^{D} X

X ⟹^{D} X

·; ⊤ ⊢ G ⟹^{G} G^{⊤} D ⟹^{D} D^{⊤}

⟹^{D}→

(G → D) ⟹^{D} G^{⊤} → D^{⊤}

[u/x]D ⟹^{D} [u/x]D^{⊤}

⟹^{D} ∀^{u}

∀x:A. D ⟹^{D} ∀x:A. D^{⊤}

\begin{aligned}D_{1} ⟹^{D} D_{1}^{⊤}  D_{2} ⟹^{D} D_{2}^{⊤} \\ & ⟹^{D} ∧ \\ D_{1} ∧ D_{2} ⟹^{D} D_{1}^{⊤} ∧ D_{2}^{⊤} \end{aligned}  \begin{aligned}D_{1} ⟹^{D} D_{1}^{⊤}  D_{2} ⟹^{D} D_{2}^{⊤} \\ & ⟹^{D} ∨ \\ D_{1} ∨ D_{2} ⟹^{D} D_{1}^{⊤} ∨ D_{2}^{⊤} \end{aligned}

Figure 1.3: ⊤-Normalization

Draft of February 28, 2000

Γ; [θ]D ⊢ [θ]Q  By hypothesis
Γ; [θ]D ⊢ [θ]D>>[θ]Q  By subderivation
D ⟹^{D} D^{⊤}  By hypothesis
Γ; [θ]D^{⊤} ⊢ [θ]D^{⊤}>>[θ]Q  By IH 2
Γ; ([θ]D^{⊤} ∧ ⊤_{q}) ⊢ [θ]D^{⊤}>>[θ]Q  By Weakening
Γ; ([θ]D^{⊤} ∧ ⊤_{q}) ⊢ [θ]Q  By rule ⊢ At
Γ; [θ]D^{⊤} ⊢ ⊤_{q} → [θ]Q  By rule ⊢→
Γ; [θ]D ⊢ [θ]Q^{⊤}  By rule At⊤ rel

Case γ ends in ⊢ At and γ′ is (AtD non-emp), (At non-rel): by IH 2.

□

Now, the converse:

Theorem 1.10 Let Γ′; D′ ⊢ G ⟹^{G} G^{⊤}, D ⟹^{D} D^{⊤}, D ⟹^{D} D^{⊤} and Γ ⊢ θ:

1. If Γ; [θ]D^{⊤} ⊢ [θ]G^{⊤}, then Γ; [θ]D ⊢ [θ]G.

2. If Γ; [θ]D^{⊤} ⊢ [θ]D^{⊤}>>[θ]Q, then Γ; [θ]D ⊢ [θ]D>>[θ]Q.

Proof: By mutual induction on the structure of γ :: Γ; [θ]D^{⊤} ⊢ [θ]G^{⊤} and δ :: Γ; [θ]D^{⊤} ⊢ [θ]D^{⊤}>>[θ]Q, as above but using ⊤-Strengthening (Lemma 1.7) in place of Weakening. □

An analogous result can be proven w.r.t. failure; the latter would require ⊤-Weakening and Strengthening w.r.t. the (immediate) denial relation. On the other hand, the above result will suffice, if we restrict to terminating programs as we do next.

1.6 Terminating Programs

We now introduce terminating programs. This is abstractly achieved by means of a relation between goals, namely G_{1} ≺ G_{2}, with the intended meaning of “G_{1} can arise as a subgoal of G_{2}”. Intuitively, a program terminates if it yields an ordering relation which admits no infinite descending chains. This is defined in Figure 1.4. We do not commit here to actual ways to verify the latter property. This issue is explored, in the higher-order setting, for example in [RP96]. More formally:

Ordering R ::= · | R, G_{1} ≺ G_{2}

Let P ⟹^{D} R and take the transitive closure of R. We say that P is terminating whenever the former is well-founded.

1.6. TERMINATING PROGRAMS  23
X ∈ {Q, ⊤, ⊥} or (dis)eq

⟹^{G} X

X ⟹^{G} ·

G ⟹^{G} R_{1} D ⟹^{D} R_{2}

⟹^{G}→

D → G ⟹^{G} R_{1}, R_{2}, G ≺ D → G

G ⟹^{G} R

⟹^{G} ∀^{y}

∀x:A. G ⟹^{G} R, [y/x]G ≺ ∀x:A. G

G ⟹^{G} R

⟹^{G} ∃

∃x:A. G ⟹^{G} R, [t/x]G ≺ ∃x:A. G

G_{1} ⟹^{G} R_{1} G_{2} ⟹^{G} R_{2}

⟹^{G} ∧

G_{1} ∧ G_{2} ⟹^{G} R_{1}, R_{2}, G_{1} ≺ G_{1} ∧ G_{2}, G_{2} ≺ G_{1} ∧ G_{2}

G_{1} ⟹^{G} R_{1} G_{2} ⟹^{G} R_{2}

⟹^{G} ∨

G_{1} ∨ G_{2} ⟹^{G} R_{1}, R_{2}, G_{1} ≺ G_{1} ∨ G_{2}, G_{2} ≺ G_{1} ∨ G_{2},

X ∈ {Q, ⊤, ⊥}

⟹^{D} X

X ⟹^{D} ·

D ⟹^{D} R_{1} G ⟹^{G} R_{2}

⟹^{D}→

(G → D) ⟹^{D} R_{1}, R_{2}, G ≺ D

D ⟹^{D} R

⟹^{D} ∀

∀x:A. D ⟹^{D} R

D_{1} ⟹^{D} R_{1} D_{2} ⟹^{D} R_{2}

⟹^{D} ∧

D_{1} ∧ D_{2} ⟹^{D} R_{1}, R_{2}

D_{1} ⟹^{D} R_{1} D_{2} ⟹^{D} R_{2}

⟹^{D} ∨

D_{1} ∨ D_{2} ⟹^{D} R_{1}, R_{2}

Figure 1.4: Generation of the Subgoal Relation Example 1.11 def(even) ⟹^{D} (even X) ≺ (even s s X). Furthermore the closure of this relation is well-founded as it can be proven say by induction on X. Consider instead the following:

Draft of February 28, 2000

∀E:exp. ∀M:nat. p (lam E) M ←

(∀x:exp. (∀N:nat. p x (s N) ← p x (s N)) → p (E x) M).

The clause is not terminating as the subgoal relation contains the pair [y/x](p x s(N) ≺ p x s(N)) which yields an infinite descending chain (p y (s 0)) ≺ (p y (s 0)) ≺ . . ..

We can now prove that if a program is terminating, a non-proof of G is a denial of G; we are going to reason classically that either there is a proof of G ground, or there is not such a proof.

Theorem 1.12 (Termination) Assume P is terminating: if not Γ; D ⊢_{P} G, then Γ; D ⊬_{P} G.

Proof: We generalize this to: let D = def(q, P ∧ D):

1. If not Γ; D ⊢_{P} G, then Γ; D ⊬_{P} G.

2. If not Γ; D ⊢_{P} D>>Q, then Γ; D ⊬_{P} >>Q.

We proceed by mutual induction on the goal ordering induced by P terminating and on the structure of D:

Case D =⊥: trivial.

Case D = ⊤.

\frac{>>⊤}{Γ; D ⊬_{P} ⊤>>Q}

Case D = D_{1} ← G_{1}. Either Γ; D ⊢_{P} G_{1} or not Γ; D ⊢_{P} G_{1} and Γ; D ⊢_{P} D_{1}>>Q or not Γ; D ⊢_{P} D_{1}>>Q. By termination G_{1} ≺ D_{1}; there are four sub-cases:

1. Γ; D ⊢_{P} G_{1}  Subcase
Γ; D ⊢_{P} D_{1}>>Q  Subcase
Γ; D ⊢_{P} D_{1} ← G_{1}>>Q  By rule >> →
2. Not Γ; D ⊢_{P} G_{1}  Subcase
Γ; D ⊬_{P} G_{1}  By IH 1
Γ; D ⊢_{P} D_{1}>>Q  Subcase
Γ; D ⊬_{P} D_{1} ← G_{1}>>Q  By rule
3. Γ; D ⊢_{P} G_{1}  Subcase
Not Γ; D ⊢_{P} D_{1}>>Q  Subcase
Γ; D ⊬_{P} D_{1}>>Q  By IH 2
Γ; D ⊬_{P} D_{1} ← G_{1}>>Q  By rule

4. Not Γ; D ⊢_{P} G_{1}  Subcase
Not Γ; D ⊢_{P} D_{1}>>Q  Subcase
Γ; D ⊬_{P} D_{1}>>Q  By IH 2
Γ; D ⊬_{P} D_{1} ← G_{1}>>Q  By rule

Case D = D_{1} ∨ D_{2}.

1. Γ; D ⊢_{P} D_{1}>>Q  Subcase
Γ; D ⊢_{P} D_{2}>>Q  Subcase
Γ; D ⊢_{P} D_{1} ∨ D_{2}>>Q  By rule >>∨
2. Γ; D ⊢_{P} D_{1}>>Q  Subcase
Not Γ; D ⊢_{P} D_{2}>>Q  Subcase
Γ; D ⊬_{P} D_{2}>>Q  By IH 2
Γ; D ⊬_{P} D_{1} ∨ D_{2}>>Q  By rule
3. Γ; D ⊢_{P} D_{2}>>Q  Subcase
Not Γ; D ⊬_{P} D_{1}>>Q  Subcase
Γ; D ⊬_{P} D_{1}>>Q  By IH 2
Γ; D ⊬_{P} D_{1} ∨ D_{2}>>Q  By rule
4. Not Γ; D ⊢_{P} D_{1}>>Q  Subcase
Not Γ; D ⊢_{P} D_{2}>>Q  Subcase
Γ; D ⊬_{P} D_{1}>>Q  By IH 2
Γ; D ⊬_{P} D_{2}>>Q  By IH 2
Γ; D ⊬_{P} D_{1} ∨ D_{2}>>Q  By rule

Case D = D_{1} ∧ D_{2}.

1. Γ; D ⊢_{P} D_{1}>>Q  Subcase
Γ; D ⊢_{P} ⊢_{P} D_{2}>>Q  Subcase
Γ; D ⊢_{P} D_{1} ∧ D_{2}>>Q  By rule >>∧
2. Γ; D ⊢_{P} D_{1}>>Q  Subcase
Not Γ; D ⊢_{P} D_{2}>>Q  Subcase
Γ; D ⊬_{P} D_{2}>>Q  By IH 2
Γ; D ⊢_{P} D_{1} ∧ D_{2}>>Q  By rule
3. Γ; D ⊢_{P} D_{2}>>Q  Subcase
Not Γ; D ⊢_{P} D_{1}>>Q  Subcase
Γ; D ⊬_{P} D_{1}>>Q  By IH 2
Γ; D ⊢_{P} D_{1} ∧ D_{2}>>Q  By rule
4. Not Γ; D ⊢_{P} D_{1}>>Q  Subcase
Γ; D ⊬_{P} D_{1}>>Q  By IH 2
Not Γ; D ⊢_{P} D_{2}>>Q  Subcase
Γ; D ⊬_{P} D_{2}>>Q  By IH 2
Γ; D ⊬_{P} D_{1} ∧ D_{2}>>Q  By rule

Case D = ∀x:A. D′. For some ground Γ ⊢ t : A, Γ; D ⊢_{P} [t/x]D′>>Q or for all ground t, not Γ; D ⊢_{P} [t/x]D′>>Q:

1. Γ; D ⊢_{P} [t/x]D′>>Q  Subcase
Γ; D ⊢_{P} ∀x:A. D′>>Q  By rule >>∀
2. For all t ground not Γ; D ⊢_{P} [t/x]D′>>Q  Subcase
For all t ground Γ; D ⊬_{P} [t/x]D′>>Q  By IH 2
Γ; D ⊬_{P} ∀x:A. D′>>Q  By rule

Case

\frac{⊬⊥}{Γ; D ⊬_{P}⊥}

Case Either Γ; D ⊢_{P} def(q, P ∧ D)>>Q or not Γ; D ⊢_{P} def(q, P ∧ D)>>Q:

1. Γ; D ⊢_{P} def(q, P ∧ D)>>Q  Subcase
Γ; D ⊢_{P} Q  By rule
2. Not Γ; D ⊢_{P} def(q, P ∧ D)>>Q  Subcase
Γ; D ⊬_{P} def(q, P ∧ D)>>Q  By IH 2
Γ; D ⊬_{P} Q  By rule

Case Either Γ; D ⊢_{P} G_{1} or not Γ; D ⊢_{P} G_{1} and either Γ; D ⊢_{P} G_{2} or not Γ; D ⊢_{P} G_{2}:

1. Γ; D ⊢_{P} G_{1}  Subcase
Γ; D ⊢_{P} G_{2}  Subcase
Γ; D ⊢_{P} G_{1} ∧ G_{2}  By rule
2. Γ; D ⊢_{P} G_{1}  Subcase
Not Γ; D ⊢_{P} G_{2}  Subcase
Γ; D ⊬_{P} G_{2}  By IH 1
Γ; D ⊬_{P} G_{1} ∧ G_{2}  By rule
3. Γ; D ⊢_{P} G_{2}  Subcase
Not Γ; D ⊢_{P} G_{1}  Subcase
Γ; D ⊬_{P} G_{1}  By IH 1
Γ; D ⊬_{P} G_{1} ∧ G_{2}  By rule
4. Not Γ; D ⊢_{P} G_{1}  Subcase
Γ; D ⊬_{P} G_{1}  By IH 1
Not Γ; D ⊢_{P} G_{2}  Subcase
Γ; D ⊬_{P} G_{2}  By IH 1
Γ; D ⊬_{P} G_{1} ∧ G_{2}  By rule

Case Either Γ; D ⊢_{P} G_{1} or not Γ; D ⊢_{P} G_{1} and either Γ; D ⊢_{P} G_{2} or not Γ; D ⊢_{P} G_{2}: Γ; D ⊬_{P} G_{2}:

1. Γ; D ⊢_{P} G_{1}  Subcase
Γ; D ⊢_{P} G_{2}  Subcase
Γ; D ⊢_{P} G_{1} ∨ G_{2}  By rule

2. Γ; D ⊢_{P} G_{1}  Subcase
Not Γ; D ⊢_{P} G_{2}  Subcase
Γ; D ⊬_{P} G_{2}  By IH 1
Γ; D ⊢_{P} G_{2} ∨ G_{1}  By rule
3. Γ; D ⊢_{P} G_{2}  Subcase
Not Γ; D ⊢_{P} G_{1}  Subcase
Γ; D ⊬_{P} G_{1}  By IH 1
Γ; D ⊢_{P} G_{2} ∨ G_{1}  By rule
4. Not Γ; D ⊢_{P} G_{1}  Subcase
Γ; D ⊬_{P} G_{1}  By IH 1
Not Γ; D ⊢_{P} G_{2}  Subcase
Γ; D ⊬_{P} G_{2}  By IH 1
Γ; D ⊬_{P} G_{1} ∨ G_{2}  By rule

Case Either for some ground Γ ⊢ t : A, Γ; D ⊢_{P} [t/x]G or for all t not Γ; D ⊢_{P} [t/x]G:

1. Γ ⊢ t : A  By hypothesis
Γ; D[t/x] ⊢_{P} G  Subcase
Γ; D ⊢_{P} ∃x:A. G  By rule
2. For all ground t not Γ; D ⊢_{P} [t/x]G  Subcase
Γ; D ⊬_{P} [t/x]G  By IH 1
Γ; D ⊬_{P} ∃x:A. G  By rule

Case For a new parameter y, (Γ, y:A); D ⊢_{P} [y/x]G or not (Γ, y:A); D ⊢_{P} [y/x]G:

1. (Γ, y:A); D ⊢_{P} [y/x]G  Subcase
Γ; [y/x]D ⊢_{P} ∀x:A. G  By rule
2. Not (Γ, y:A); D ⊢_{P} [y/x]G  Subcase
(Γ, y:A); D ⊢_{P} [y/x]G  By IH 1
Γ; [, y/x]D ⊬_{P} ∀x:A. G  By rule

Case Γ; (D ∧ D) ⊢_{P} G or not Γ; (D ∧ D) ⊢_{P} G:

1. Γ; (D ∧ D) ⊢_{P} G  Subcase
Γ; D ⊢_{P} D → G  By rule
2. Not Γ; (D ∧ D) ⊢_{P} G  Subcase
Γ; (D ∧ D) ⊬_{P} G  By IH 1
Γ; D ⊬_{P} D → G  By rule

Case The (dis)equality case follows immediately from the decidability of the

=^{·}, ≠^{·} rules.

□

1.7 Context Schemata

In this Section, we address the properties of contexts^{2}. We restrict to secondorder programs, specifically to programs which make only Horn assumptions; this is enough to achieve satisfaction of boolean axioms for the algebra of clause complementation.

Hereditary Harrop formulae differ form Horn clauses in that they may dynamically extend the current signature and program; this is reflected in the provability (and denial) relation which is parameterized by a run-time context Γ; D. As we have argued before (Section 1.4) we cannot obtain closure under clause complementation for the full logic of hhf, but we have to restrict to a smaller (but significant) fragment. This in turn entails that we have to make sure that during execution whenever an assumption is made, the latter stays in the fragment we have isolated. Technically, we proceed as follows:

• We extract from the static definition of a predicate the general ‘template’ of a legal assumption.

• We require dynamic assumptions to conform to this template.

We thus introduce the notion of schema satisfaction; we will need the following data structure: a schema context abstracts over all possible instantiation of a run-time context. To account for that, we introduce a quantifier-like operator, say SOME Φ .D, which takes a clause and existentially bounds its free variables, i.e. Φ = F V (D). As usual, we implicitly annotate those variables with their types. This is achieved by the following reification of schemata. Do not confuse ‘∥’, which is used to represent schema alternatives in the object language with ‘|’ which does the same in our informal meta-language.

Contexts Schemata S ::= ∘ | S∥(Γ; SOME Φ .D)

We will also need to disambiguate blocks in run-time contexts; overlapping may indeed happen when the alternatives in a context schema are not disjoint. To achieve that, we simply modify the provability and denial rules ⊢ At and ⊬ At by ‘packaging’ run-time contexts into blocks with a bracket operator ⌈ ⌉. Intuitively, a block is complete when an atomic conclusion is reached during the deduction. It is therefore bracketed when the run-time context is passed to the immediate implication judgment.

⌈Γ⌉; ⌈D⌉ ⊢_{P} def(Q, P ∧ D)>>Q
⊢ At Γ; D ⊢_{P} Q
⌈Γ⌉; ⌈D⌉ ⊬_{P} def(Q, P ∧ D)>>Q
⊬ At
Γ; D ⊬_{P} Q

2This section is inspired by Schürmann’s treatment of similar material in his forthcoming dissertation [].

Draft of February 28, 2000

Still, we need to ‘flatten’ blocks, so that re-bracketing during execution will be immaterial on already delimited blocks; we thus require the bracket operator to satisfy the following absorption-distribution law:

⌈⌈Γ⌉, Γ′⌉ = ⌈Γ⌉, ⌈Γ′⌉
⌈⌈D⌉ ∧ D′⌉ = ⌈D⌉ ∧ ⌈D′⌉

We are now ready to define when a run-time context is an instance of a schema. First, we say that a completed block occurs in a schema when the block is an alphabetic variant of some instantiation of one of the alternatives of the schema. We restrain from giving rules for substitutions; we simply mention that the codomain is Φ, i.e. the global parameters introduced by the ⊧_{S} ∀ and \∃ rules, while the domain is Γ.

(Γ′; D′) ≡_{α} (Γ; θD) ∈_{1}

(Γ′; D′) ∈ S∥(Γ; SOME Φ .D)

\begin{aligned}(Γ′; D′) ∈ S \\ & ∈_{2} \\ (Γ′; D′) ∈ S∥(Γ; D) \end{aligned}

Let us now analyze the rules in Figure 1.5. The empty run-time context is an instance of every schema. Moreover if Γ′ and D′ are completed blocks which occur in S, as denoted by the block notation then (Γ, ⌈Γ′⌉); (D ∧ ⌈D′⌉) is an instance of S, provided that D′ is a valid clause. Thus we need to define the instance relation simultaneously to clause (and in turn to goal) satisfaction. The judgment ⊧_{S} D is merely auxiliary to the Γ; D \ G < S one: here we mimic the construction on the run-time schema until in the base case we check whether the resulting context is an instance of the given schema.

1.7.1 Schema Extraction

Roughly, we extract a context schema by collecting all negative occurrences in a goal: this is achieved by the judgment Γ; D ⊢ G ⟹^{G} S. The latter is mutually recursive to the judgment D ⟹^{D} S which collects schemata for each clause in the given program, as depicted in Figure 1.6. When an atomic goal is reached, the current list of parameter and assumption is returned, with the correct existential binding. We make the convention to absorb schema alternatives which are αvariants. Moreover the empty run-time context behave as a left and right zero element for ∥, i.e.

(Γ; D∥·; ⊤) = (·; ⊤∥)Γ; D = Γ; D

Finally ∥ is commutative.

We aim to show that if a schema context is extracted by a program, the latter satisfies the former. First, we need to establish two weakening lemmata w.r.t. schema alternatives:

Lemma 1.13 If Γ; D ∈ S then Γ; D ∈ S′∥S.

Proof: By a straightforward induction on the structure of π :: Γ; D ∈ S. □

X ∈ {Q, ⊤, ⊥} or (dis)eq Γ; D < S

\X

Γ; D \ X < S

Γ; D \ G_{1} < S Γ; D \ G_{2} < S

\∧

Γ; D \ G_{1} ∧ G_{2} < S

Γ; D \ G_{1} < S Γ; D \ G_{2} < S

\∨

Γ; D \ G_{1} ∨ G_{2} < S
Γ; D \ [u/x]G < S
\∃^{u}
Γ; D \ ∃x:A. G < S
(Γ, y:A); D \ [y/x]G < S

\∀^{y}

Γ; D \ ∀x:A. G < S

⊧_{S} D Γ; (D ∧ D) \ G < S

\ →

Γ; D \ D → G < S

X ∈ {Q, ⊤ ⊥}

⊧_{S} X

⊧_{S} X

⊧_{S} D_{1} ⊧_{S} D_{2}
⊧_{S} ∧

⊧_{S} D_{1} ∧ D_{2}

⊧_{S} D_{1} ⊧_{S} D_{2}
⊧_{S} ∨

⊧_{S} D_{1} ∨ D_{2}

\begin{aligned}⊧_{S} [u/x]D \\ & ⊧_{S} ∀^{u} \\ ⊧_{S} ∀x:A. D \end{aligned}

⊧_{S} D ·; ⊤ \ G < S

⊧_{S}→

⊧_{S} G → D

\frac{<_{1}}{·; ⊤ < S}  \begin{aligned}(Γ′; D′) ∈ S ⊧_{S} D′ (Γ; D) < S \\ & <_{2} \\ (Γ, ⌈Γ′⌉); (D ∧ ⌈D′⌉) < S \end{aligned}

Figure 1.5: Judgments Γ; D \ G < S, ⊧_{S} D and Γ; D < S

Draft of February 28, 2000

X ∈ {Q, ⊤, ⊥} or (dis)eq F V (D) = Φ

⟹^{G} X

Γ; D ⊢ X ⟹^{G} Γ; SOME Φ .D

Γ; (D ∧ D) ⊢ G ⟹^{G} S_{1} D ⟹^{D} S_{2}

⟹^{G}→

Γ; D ⊢ D → G ⟹^{G} S_{1}∥S_{2}

(Γ, y:A); D ⊢ [y/x]G ⟹^{G} S

⟹^{G} ∀^{y}

Γ; D ⊢ ∀x:A. G ⟹^{G} S

Γ; D ⊢ [u/x]G ⟹^{G} S

⟹^{G} ∃^{y}

Γ; D ⊢ ∃x:A. G ⟹^{G} S

Γ; D ⊢ G_{1} ⟹^{G} S_{1} Γ; D ⊢ G_{2} ⟹^{G} S_{2}

⟹^{G} ∧

Γ; D ⊢ G_{1} ∧ G_{2} ⟹^{G} S_{1}∥S_{2}

Γ; D ⊢ G_{1} ⟹^{G} S_{1} Γ; D ⊢ G_{2} ⟹^{G} S_{2}

⟹^{G} ∨

Γ; D ⊢ G_{1} ∨ G_{2} ⟹^{G} S_{1}∥S_{2}

X ∈ {Q, ⊤, ⊥}

⟹^{D} X

X ⟹^{D} ·; ⊤

·; ⊤ ⊢ G ⟹^{G} S_{1} D ⟹^{D} S_{2}

⟹^{D}→

(G → D) ⟹^{D} S_{1}∥S_{2}

[u/x]D ⟹^{D} S

⟹^{D} ∀^{y}

∀x:A. D ⟹^{D} S

D_{1} ⟹^{D} S_{1} D_{2} ⟹^{D} S_{2}

⟹^{D} ∧

D_{1} ∧ D_{2} ⟹^{D} S_{1}∥S_{2}

D_{1} ⟹^{D} S_{1} D_{2} ⟹^{D} S_{2}

⟹^{D} ∨

D_{1} ∨ D_{2} ⟹^{D} S_{1}∥S_{2}

Figure 1.6: Extracting Contexts Schemata

Draft of February 28, 2000

32  CHAPTER 1. CLAUSE COMPLEMENTATION

Note also that Γ; D ∈ S′∥S iff Γ; D ∈ S∥S′. Lemma 1.14 (Schema Weakening) Let Γ; D < S. Then

1. If ⊧_{S} D, then ⊧_{S∥S′} D.

2. If Γ; D \ G < S, then Γ; D \ G < S∥S′.

3. If Γ; D < S then Γ; D < S∥S′. Proof: By mutual induction on the structure of π :: ⊧_{S} D, γ :: Γ; D \ G < S and σ :: Γ; D < S. We show the crucial cases: Case

π = \begin{aligned}X ∈ \{Q, ⊤, ⊥\} \\ & ⊧_{S} X \\ ⊧_{S} X \end{aligned}

Trivially

π′ = \begin{aligned}X ∈ \{Q, ⊤, ⊥\} \\ & ⊧_{S} X \\ ⊧_{S∥S′} Q \end{aligned}

Case

π = \begin{aligned}⊧_{S} D ·; ⊤ \ G < S \\ & ⊧_{S}→ \\ ⊧_{S} G → D \end{aligned}

⊧_{S} D  By subderivation
⊧_{S∥S′} D  By IH 1
·; ⊤ \ G < S  By subderivation
·; ⊤ \ G < S∥S′  By IH 2
⊧_{S∥S′} G → D  By rule ⊧_{S}→

Case

γ = X ∈ {Q, ⊤, ⊥} or (dis)eq Γ; D < S \X Γ; D \ X < S
Γ; D < S  By subderivation
Γ; D < S∥S′  By IH 3
Γ; D \ X < S∥S′  By rule \X

Case

γ = \begin{aligned}⊧_{S} D Γ; D ∧ D \ G < S \\ & \ → \\ Γ; D \ D → G < S \end{aligned}

⊧_{S} D  By subderivation
⊧_{S∥S′} D  By IH 1
Γ; D ∧ D \ G < S  By subderivation
Γ; (D ∧ D) \ G < S∥S′  By IH 2
Γ; D \ D → G < S∥S′  By rule \ →

Draft of February 28, 2000

Case

σ = \frac{<_{1}}{·; ⊤ < S}

Then immediately:

σ′ = \frac{<_{1}}{·; ⊤ < S∥S′}

Case

σ = \begin{aligned}(Γ′; D′) ∈ S ⊧_{S} D′ (Γ; D) < S \\ & <_{2} \\ (Γ, ⌈Γ′⌉); (D ∧ ⌈D′⌉) < S \end{aligned}

Γ; D < S  By subderivation
Γ; D < S∥S′  By IH 3
Γ′; D′ ∈ S  By subderivation
Γ′; D′ ∈ S∥S′  By Lemma 1.13
⊧_{S} D′  By subderivation
⊧_{S∥S′} D  By IH 1
(Γ, ⌈Γ′⌉); (D ∧ ⌈D′⌉) < S∥S′  By rule <_{2}
□

We are now ready to show that if a program yields a schema, then every instance of a clause used at run-rime will comply with the schema. We need to generalize this statement to take into account instances of goals as well; in the latter case, we need to synchronize the schema accumulator in Γ′; D′ ⊢ G ⟹^{G} S with the possibly incomplete run-time context Γ; D. A fortiori the result holds for compile-time contexts as well, by taking Γ; D as ·; ⊤.

Theorem 1.15 (Extracted Schema Satisfaction) Let Γ ⊢ θ, where dom(θ) = F V (D′) ∪ F V (D):

1. If D ⟹^{D} S, then ⊧_{S} [θ]D.

2. If Γ′; D′ ⊢ G ⟹^{G} S, ⊧_{S} [θ]D′ and Γ; D < S, then (Γ, Γ′); (D∧[θ]D′\[θ]G < S.

Proof: By mutual induction on the structure of π :: D ⟹^{D} S and γ :: Γ′; D′ ⊢

G ⟹^{G} S.

Case

π = \begin{aligned}X ∈ \{Q, ⊤, ⊥\} \\ & ⟹^{D} X \\ X ⟹^{D} ·; ⊤ \end{aligned}

⊧_{·;⊤} X  By rule ⊧_{S} X

Draft of February 28, 2000

Case

π = \begin{aligned}D_{1} ⟹^{D} S_{1} D_{2} ⟹^{D} S_{2} \\ & ⟹^{D} ∧ \\ D_{1} ∧ D_{2} ⟹^{D} S_{1}∥S_{2} \end{aligned}

D_{1} ⟹^{D} S_{1}  By subderivation
D_{2} ⟹^{D} S_{2}  By subderivation
⊧_{S_{1}} [θ]D_{1}  By IH 1
⊧_{S_{2}} [θ]D_{2}  By IH 1
⊧_{S_{1}∥S_{2}} [θ]D_{1}  By Lemma 1.14
⊧_{S_{1}∥S_{2}} [θ]D_{2}  By Lemma 1.14
⊧_{S_{1}∥S_{2}} [θ]D_{1} ∧ [θ]D_{2}  By rule ⊧_{S} ∧
⊧_{S_{1}∥S_{2}} [θ](D_{1} ∧ D_{2})  By subst.

Case π ends in ⟹^{D} ∨: analogously to the above. Case π ends in ⟹^{D} ∀^{y}: by an immediate appeal to IH 1. Case

π = \begin{aligned}·; ⊤ ⊢ G ⟹^{G} S_{1} D ⟹^{D} S_{2} \\ & ⟹^{D}→ \\ (G → D) ⟹^{D} S_{1}∥S_{2} \end{aligned}

D ⟹^{D} S_{2}  By subderivation
⊧_{S_{2}} [θ]D  By IH 1
⊧_{S_{1}∥S_{2}} [θ]D  By Lemma 1.14
·; ⊤ ⊢ G ⟹^{G} S_{1}  By subderivation
·; ⊤ < S_{1}  By rule <_{1}
·; ⊤ \ [θ]G < S_{1}  By IH 2
·; ⊤ \ [θ]G < S_{1}∥S_{2}  By Lemma 1.14
⊧_{S_{1}∥S_{2}} [θ]G → [θ]D  By rule ⊧_{S}→

Case

γ = X ∈ {Q, ⊤, ⊥} or (dis)eq F V (D′) = Φ ⟹^{G} X Γ′; D′ ⊢ X ⟹^{G} Γ′; SOME Φ .D′

Γ′; [θ]D′ ≡_{α} Γ′; [θ]D′  By hypothesis
Γ′; [θ]D′ ∈ Γ′; SOME Φ .D′  By rule ∈_{1}
Γ; D < Γ′; SOME Φ .D′  By hypothesis
⊧_{Γ′;SOME Φ .D′} [θ]D′  By hypothesis
(Γ, Γ′); (D ∧ [θ]D′) < Γ′; SOME Φ .D′  By rule <_{2}
(Γ, Γ′); (D ∧ [θ]D′) \ [θ]X < Γ′; SOME Φ .D′  By rule \X

Case

γ = \begin{aligned}(Γ′, y:A); D′ ⊢ [y/x]G ⟹^{G} S \\ & ⟹^{G} ∀^{y} \\ Γ′; D′ ⊢ ∀x:A. G ⟹^{G} S \end{aligned}

Draft of February 28, 2000

(Γ′, y:A); D′ ⊢ [y/x]G ⟹^{G} S  By subderivation
(Γ, Γ′, y:A); (D ∧ [θ]D′) \ [θ] · [y/x]G < S  By IH 2
(Γ, Γ′); (D ∧ [θ]D′) \ [θ]∀x:A. G < S  By rule \∀^{y}

Case

γ = \begin{aligned}Γ′; (D′ ∧ D) ⊢ G ⟹^{G} S_{1} D ⟹^{D} S_{2} \\ & ⟹^{G}→ \\ Γ′; D′ ⊢ D → G ⟹^{G} S_{1}∥S_{2} \end{aligned}

D ⟹^{D} S_{2}  By subderivation
⊧_{S_{2}} [θ]D  By IH 1
⊧_{S_{1}∥S_{2}} [θ]D  By Lemma 1.14
Γ; D < S_{1}  By hypothesis
Γ′; (D′ ∧ D) ⊢ G ⟹^{G} S_{1}  By subderivation
(Γ, Γ′); (D ∧ [θ]D′ ∧ [θ]D) \ [θ]G < S_{1}  By IH 2
(Γ, Γ′); (D ∧ [θ]D′ ∧ [θ]D) \ [θ]G < S_{1}∥S_{2}  By Lemma 1.14
(Γ, Γ′); (D ∧ [θ]D′) \ [θ]D → [θ]G < S_{1}∥S_{2}  By rule \ →

Case

γ = \begin{aligned}Γ′; D′ ⊢ G_{1} ⟹^{G} S_{1} Γ′; D′ ⊢ G_{2} ⟹^{G} S_{2} \\ & ⟹^{G} ∧ \\ Γ′; D′ ⊢ G_{1} ∧ G_{2} ⟹^{G} S_{1}∥S_{2} \end{aligned}

Γ′; D′ ⊢ G_{1} ⟹^{G} S_{1}  By subderivation
Γ; D < S_{1}  By hypothesis
(Γ, Γ′); (D ∧ [θ]D′) \ [θ]G_{1} < S_{1}  By IH 2
(Γ, Γ′); (D ∧ [θ]D′) \ [θ]G_{1} < S_{1}∥S_{2}  By Lemma 1.14
Γ′; D′ ⊢ G_{2} ⟹^{G} S_{2}  By subderivation
Γ; D < S_{2}  By hypothesis
(Γ, Γ′); (D ∧ [θ]D′) \ [θ]G_{2} < S_{2}  By IH 2
(Γ, Γ′); (D ∧ [θ]D′) \ [θ]G_{2} < S_{1}∥S_{2}  By Lemma 1.14
(Γ, Γ′); (D ∧ [θ]D′) \ [θ]G_{1} ∧ [θ]G_{2} < S_{1}∥S_{2}  By rule \∧

Case γ ends in ⟹^{G} ∨: similarly to the above.

Case γ ends in ⟹^{G} ∃^{y}: by an immediate appeal to IH 2.

□

1.7.2 Context Preservation

We aim to prove that execution preserves contexts, i.e. that every subgoal which arises in any given successful or failed (immediate and non-immediate sub-derivation) satisfies the context schema.

The following Lemma ensures that when an assumption D is pulled from a legal run-time context, i.e. which satisfies a given schema, so does D.

Lemma 1.16 If Γ; D < S and D ∈ D, then ⊧_{S} D. Proof: By induction on the structure of the derivation of π :: Γ; D < S. Case

π = \frac{<_{1}}{·; ⊤ < S}

Then D = ⊤ and immediately

π′ = \frac{⊧_{S} ⊤}{·; ⊤ ⊧_{S} ⊤}

Case

π = \begin{aligned}(Γ′; D′) ∈ S ⊧_{S} D′ (Γ′′; D′′) < S \\ & <_{2} \\ (Γ′′, ⌈Γ′⌉); (D′′ ∧ ⌈D′⌉) < S \end{aligned}

Subcase D ≡ D′
⊧_{S} D′  By hypothesis
Subcase D ∈ D′′
Γ′′; D′′ < S  By subderivation
⊧_{S} D  By IH
□

Finally, the proof of context preservation; note that we have already established schema extraction (Theorem 1.15), that is we assume that P ⟹^{D} S. Theorem 1.17 (Context Preservation w.r.t. Provability) Let ⊧_{S} P and D ∈ def(Q, P ∧ D). For any Γ; D < S, if (π :: Γ; D ⊢_{P} G and Γ; D \ G < S) or (ι :: Γ; D ⊢_{P} D>>Q and ⊧_{S} D), then:

1. for every subproof π′ :: Γ′; D′ ⊢_{P} G′ and Γ′; D′ \ G′ < S.

2. for every subproof ι′ :: Γ′; D′ ⊢_{P} D′>>Q and ⊧_{S} D′. Proof: By mutual induction on the structure of π :: Γ; D ⊢_{P} G and ι :: Γ; D ⊢_{P} D>>Q. Case π ends in Γ; D ⊢_{P} ⊤: trivial. Case π ends in Γ; D ⊢_{P} D → G:

Γ; D ∧ D ⊢_{P} G  By subderivation
Γ; D \ D → G < S  By hypothesis
Γ; D ∧ D \ G < S  By inversion
for any ι′ :: Γ′; D′ ⊢_{P} D′>>Q and ⊧_{S} D′ and
for any π′ :: Γ′; (D′ ∧ D′) ⊢_{P} G′ and Γ′; (D′ ∧ D′) \ G′ < S  By IH
for any π′ :: Γ′; D′ ⊢_{P} D′ → G′ and Γ′; D′ \ D → G′ < S  By rule

Draft of February 28, 2000

Case π ends in Γ; D ⊢_{P} ∀x:A. G:

(Γ, y:A); D ⊢_{P} [y/x]G  By subderivation
Γ; D \ ∀x:A. G < S  By hypothesis
(Γ, y:A); D \ [y/x]G < S  By inversion

for any ι′ :: Γ′; D′ ⊢_{P} D′>>Q and ⊧_{S} D′ and

for any π′ :: (Γ′, y:A); D′ ⊢_{P} [y/x]G′ and (Γ′, y:A); D′ \ [y/x]G′ < S By IH

for any π′ :: Γ′; D′ ⊢_{P} ∀x:A. G′ and Γ′; D′ \ ∀x:A. G′ < S br

Case π ends in ⊢ ∧, ⊢ ∨_{1}, ⊢ ∨_{2}, ⊢ ∃: similarly by IH.

Case π ends in Γ; D ⊢_{P} Q:

Subcase ι :: Γ; D ⊢_{P} D>>Q, for D ∈ def(Q, P)  By subderivation
⊧_{S} D  By hypothesis
for any π′ :: Γ′; D′ ⊢_{P} G′ and Γ′; D′ \ G′ < S and
for any ι′ :: Γ′; D′ ⊢_{P} D′>>Q and ⊧_{S} D′  By IH
Subcase ι :: Γ; D ⊢_{P} D>>Q, for D ∈ def(Q, D)  By subderivation
⊧_{S} D  By Lemma 1.16
for any π′ :: Γ′; D′ ⊢_{P} G′ and Γ′; D′ \ G′ < S and
for any ι′ :: Γ′; D′ ⊢_{P} D′>>Q and ⊧_{S} D′  By IH

Case ι :: Γ; D ⊢_{P}⊥ >>Q: trivial.

Case ι :: Γ; D ⊢_{P} D_{1} ∧ D_{2}>>Q:

⊧_{S} D_{1} ∧ D_{2}  By hypothesis
⊧_{S} D_{1} and ⊧_{S} D_{2}  By inversion
Subcase Γ; D ⊢_{P} D_{1}>>Q  By subderivation
for any π′ :: Γ′; D′ ⊢_{P} G′ and Γ′; D′ \ G′ < S and
for any ι′ :: Γ′; D′ ⊢_{P} D′_{1}>>Q and ⊧_{S} D′_{1}  By IH
for any ι′ :: Γ′; D′ ⊢_{P} D′_{1} ∧ D′_{2}>>Q and ⊧_{S} D′_{1} ∧ D′_{2}  By rule
Subcase Γ; D ⊢_{P} D_{2}>>Q  Symmetrical

Case ι :: Γ; D ⊢_{P} ∀x:A. D>>Q

Γ; D ⊢_{P} [t/x]D>>Q  By subderivation
⊧_{S} ∀x:A. D  By hypothesis
⊧_{S} [u/x]D  By inversion
⊧_{S} [t/u, u/x]D  By substitution

for any π′ :: Γ′; D′ ⊢_{P} G′ and Γ′; D′ \ G′ < S and

for any ι′ :: Γ′; D′ ⊢_{P} [t/x]D′>>Q and ⊧_{S} [t/x]D′  By IH
for any ι′ :: Γ′; D′ ⊢_{P} ∀x:A. D′>>Q and ⊧_{S} ∀x:A. D′  By rule

Case ι :: Γ; D ⊢_{P} G → D>>Q:

Γ; D ⊢_{P} D>>Q and Γ; D ⊢_{P} G  By subderivation
⊧_{S} G → D  By hypothesis
Γ; D \ G < S and ⊧_{S} D  By inversion

for any π′ :: Γ′; D′ ⊢_{P} G′ and Γ′; D′ \ G′ < S and

for any ι′ :: Γ′; D′ ⊢_{P} D′>>Q and ⊧_{S} D′  By IH
for any ι′ :: Γ′; D′ ⊢_{P} G′ → D′>>Q and ⊧_{S} G′ → D′  By rule

Case ι ends in >>∨, >>∀: similarly by IH.

□

An analogous result is easily established w.r.t. denial. We recall that the statement must be generalized to account for the meta-level extensional quantification brought in by the ≯>∀, ⊬ ∃ rules; at the same time those substitution terms should be disjoint with the global parameters which are instantiated while satisfying the schema.

Theorem 1.18 (Context Preservationw.r.t. Denial) Let θ be a well-typed substitution such that Γ ⊢ θ and x ∉ dom(θ) and cod(θ) ∩ F V (D) = ∅. Let ⊧_{S} P and D ∈ def(Q, P ∧ D); for any Γ; [θ]D < S, if ( π :: Γ; [θ]D ⊬_{P} [θ]G and Γ; [θ]D \ [θ]G < S ) or ( ι :: Γ; [θ]D ⊬_{P} [θ]D>>[θ]Q and ⊧_{S} [θ]D), then for all [θ]′:

1. for every subproof π′ :: Γ′; [θ]′D′ ⊬_{P} [θ′]G′ and Γ′; [θ]′D′ \ [θ′]G′ < S.

2. for every subproof ι′ :: Γ′; [θ]′D′ ⊬_{P} [θ′]D′>>[θ′]Q and ⊧_{S} [θ′]D′.

Proof: By mutual induction on the structure of π :: Γ; [θ]D ⊬_{P} [θ]G and ι :: Γ; [θ]D ⊬_{P} [θ]D>>[θ]Q, as above. We show only some cases:

Case

π = for all n, [θ] Γ ⊢ n : A Γ; [θ]D ⊬_{P} [θ, n/x]G ⊬ ∃ for all [θ] Γ; [θ]D ⊬_{P} [θ]∃x:A. G

for all [θ] , n Γ; [θ]D ⊬_{P} [θ, n/x]G  By subderivation
for all [θ] \ [θ]∃x:A. G < S  By hypothesis
for all [θ] \ [θ, u/x]G < S  By inversion
for all [θ] , n \ [θ, n/u, u/x]G  By substitution

for any ι′ :: Γ′; [θ]′D′ ⊬_{P} [θ′]D′>>[θ′]Q and ⊧_{S} [θ′]D′ and

for any π′ :: Γ′; [θ]′D′ ⊬_{P} [θ′, n/x]G′ and Γ′; [θ]′D′ \ [θ′, n/x]G′ < S By IH
for any π′ :: Γ′; [θ]′D′ ⊬_{P} [θ′]∃x:A. G′ and Γ′; [θ]′D′ \ [θ′]∃x:A. G′ < S By rule

Case

π = for all [θ] Γ; ([θ]D ∧ [θ]D) ⊬_{P} [θ]G ⊬ → Γ; [θ]D ⊬_{P} [θ]D → [θ]G

Draft of February 28, 2000

for all [θ] Γ; ([θ]D ∧ [θ]D) ⊬_{P} [θ]G  By subderivation
for all [θ] Γ; [θ]D \ [θ]D → [θ]G < S  By hypothesis
for all [θ] Γ; [θ]D ∧ [θ]D \ [θ]G < S  By inversion

for any ι′ :: Γ′; [θ]′D′ ⊬_{P} [θ′]D′>>[θ′]Q and ⊧_{S} [θ′]D′ and

for any π′ :: Γ; ([θ′]D′ ∧ [θ′]D′) ⊬_{P} [θ′]G′ and Γ; ([θ′]D′ ∧ [θ′]D′) \ [θ′]G′ < S By IH
for any π′ :: Γ′; [θ]′D′ ⊬_{P} [θ′](D′ → G′) and Γ′; [θ]′D′ \ [θ′](D′ → G′) < S By rule

Case

ι = for all [θ] Γ; [θ]D ⊬_{P} [θ]G ≯>→_{1} for all [θ] Γ; [θ]D ⊬_{P} [θ]D ← [θ]G>>[θ]Q

for all [θ] Γ; [θ]D ⊬_{P} [θ]G  By subderivation
for all [θ] ⊧_{S} [θ]G → [θ]D  By hypothesis
for all [θ] Γ; [θ]D \ [θ]G < S and ⊧_{S} [θ]D  By inversion

for any π′ :: Γ′; [θ]′D′ ⊢_{P} G′ and Γ′; [θ]′D′ \ G′ < S and

for any ι′ :: Γ′; [θ]′D′ ⊢_{P} [θ′]D′>>[θ′]Q and ⊧_{S} [θ′]D′  By IH
for any ι′ :: Γ′; [θ]′D′ ⊬_{P} [θ′](D′ ← G′)>>[θ′]Q and ⊧_{S} [θ′](D′ ← G′)By rule

Case

ι = for all [θ] Γ; [θ]D ⊬_{P} [θ]D>>[θ]Q ≯>→_{2} for all [θ] Γ; [θ]D ⊬_{P} [θ]D ← [θ]G>>[θ]Q

for all [θ] Γ; [θ]D ⊬_{P} [θ]D>>[θ]Q  By subderivation
for all [θ] ⊧_{S} [θ]G → [θ]D  By hypothesis
for all [θ] Γ; [θ]D \ [θ]G < S and ⊧_{S} [θ]D  By inversion

for any π′ :: Γ′; [θ]′D′ ⊬_{P} [θ′]G′ and Γ′; [θ]′D′ \ [θ′]G′ < S and

for any ι′ :: Γ′; [θ]′D′ ⊬_{P} [θ′]D′>>[θ′]Q and ⊧_{S} [θ′]D′  By IH
for any ι′ :: Γ′; [θ]′D′ ⊬_{P} [θ′](D′ ← G′)>>[θ′]Q and ⊧_{S} [θ′](D′ ← G′)By rule
□

1.8 Clause Complementation

We restrict to programs with:

• Complementable clauses of the form Q ← G such that the head of every term in Q is rigid.

• Parameters of base type and occurring only in head position, called Shallow Parameter Expressions.

We do not formalize here the former assumptions on terms; note that the constructor restriction applies only to non-Horn predicate definitions and can be relaxed significantly, see the comment and the end of the proof of Theorem 1.27. We do give a definition of complementable clause in Figure 1.7.

40  CHAPTER 1. CLAUSE COMPLEMENTATION
X ∈ {⊤, ⊥} or (dis)eq

G X Γ; D ⊢ X compl

\frac{At}{Γ; ⊤ ⊢ Q compl} D ∈ D → dom(Γ) ∩ par(D) ≠ ∅

At∩

Γ; D ⊢ Q compl

Γ; (D ∧ D) ⊢ G compl D compl

→

Γ; D ⊢ D → G compl
(Γ, y:a); D ⊢ [y/x]G compl

∀^{y} ∀x:a. G compl

Γ; D ⊢ G_{1} compl Γ; D ⊢ G_{2} compl

∧

Γ; D ⊢ G_{1} ∧ G_{2} compl

Γ; D ⊢ G_{1} compl Γ; D ⊢ G_{2} compl

∨

Γ; D ⊢ G_{1} ∨ G_{2} compl

\begin{aligned}X ∈ \{⊤, ⊥\} \\ & D X \\ X compl \end{aligned}

·; ⊤ ⊢ G compl ←

Q ← D compl [u/x]D compl

∀^{u} ∀x:A. D compl

D_{1} compl D_{2} compl

∧
D_{1} ∧ D_{2} compl
D_{1} compl D_{2} compl
∨
D_{1} ∨ D_{2} compl

Figure 1.7: Complementable clause and goal: D compl and Γ; D ⊢ G compl

Draft of February 28, 2000

Example 1.19 The clause encoding the introduction rule for implication in natural deduction from Example 1.1 is not complementable:

impi : nd(A imp B) ← (nd(A) → nd(B)).

On the other hand, the following is allowed by rule At:

oplam^{⊤} : ∀E:exp → exp. open (lam E)
← (∀x:exp. ⊤_{open} → open (E x)).

The same rule promotes the following:

isdall : ∀D:term → form. isd (all D) ←
∀x:term. isd (D x).

The restriction on goal and clause yields this revised grammar:

Clauses D ::= ⊤ |⊥| Q ← G | D_{1} ∧ D_{2} | D_{1} ∨ D_{2} | ∀x:a. D
Goals G ::= Q | ⊤ |⊥| M⃗ =^{·} N⃗ | M⃗ ≠^{·} N⃗ |
G_{1} ∧ G_{2} | G_{1} ∨ G_{2} | D → G | ∀x:a. G

Note that ‘facts’ are represented, in a standardized way, by Q ← ⊤, although in examples we will omit to mention the body if it is ⊤. We accordingly specialize the immediate implication and denial rules as follows:

Γ; D ⊢_{P} N⃗ =^{·} M⃗ Γ; D ⊢_{P} G >> →

Γ; D ⊢_{P} (q N⃗ ← G)>>q M⃗

Γ; D ⊬_{P} N⃗ ≠^{·} M⃗ ⊬_{P} G

≯>→_{2}

Γ; D ⊬_{P} (q N⃗ ← G)>>q M⃗

Γ; D ⊬_{P} N⃗ =^{·} M⃗

≯>→_{1}
Γ; D ⊬_{P} (q N⃗ ← G)>>q M⃗

We remark that the ‘guards’ in the immediate denial rules are constructed so as to make the positive and negative judgment mutually independent. Thus ≯> →_{1} says that a clause q N⃗ ← G denies a goal q M⃗ if N⃗ and M⃗ clashes. Rule ≯> →_{2} instead attributes denial with the same conclusion due to ‘failure’ in the body. If we use ∀(D) to denote the universal closure of (all) the free variables in D, then following is a derived rule of inference:

Γ ⊢ σ Γ; D ⊢_{P} σN⃗ =^{·} M⃗

∀σ>>

Γ; D ⊢_{P} ∀(q N⃗ ← ⊤)>>q M⃗

As it can be proven by a straightforward induction on the number of free variables in N⃗.

\frac{Not_{D}⊤}{Not_{D}(⊤) =⊥}
\frac{Not_{D} ⊥}{Not_{D}(⊥) = ⊤}
Not_{G}(G) = G′
Not_{D} ←

Not_{D}(q M⃗ ← G) = ⋀_{N⃗∈Not(M⃗)} ∀(¬(q N⃗) ← ⊤) ∧ (¬q M⃗ ← G′)

Not_{D}(D) = D′
Not_{D}∀
Not_{D}(∀x:A. D) = ∀x:A. D′
Not_{D}(D_{1}) = D′_{1} Not_{D}(D_{2}) = D′_{2}
Not∧
Not_{D}(D_{1} ∧ D_{2}) = D′_{1} ∨ D′_{2}
Not_{D}(D_{1}) = D′_{1} Not_{D}(D_{2}) = D′_{2}
Not∨
Not_{D}(D_{1} ∨ D_{2}) = D′_{1} ∧ D′_{2}

Figure 1.8: Clause Complementation: Not_{D}(D) = D′

We now introduce in Figure 1.8 and Figure 1.9 the rules for static and dynamic clause complementation. Consider a rule q M⃗ ← G ∈ def(q); its complement must contain a ‘factual’ part motivating failure due to clash with the head; the remainder Not_{G}(G) expresses failure in the body, if any. Clause complementation must discriminate whether this rule belongs to the static or dynamic definition of a predicate. In the first case all the relevant information is already present in the head of the clause and we can use the term complementation algorithm described in Chapter ??. This is accomplished by the rule Not_{D} →, where a set of negative facts is built via term complementation Not(M⃗), namely ⋀_{N⃗∈Not(M⃗)} ∀(¬(q N⃗) ← ⊤), whose fresh free variables are universally closed; moreover the negative counterpart of the source clause is obtained via complementation of the body. The original quantification is retained thanks to rule Not_{D}∀.

Otherwise, we can think of complementation of assumptions, which are by definition parametric in some x, as static clause complementation w.r.t. x. Informally, for an atomic assumption, say q M_{1} … M_{i−1} e_{x} M_{i+1} … M_{n}, its complement can be taken as Not_{D}(q_{e_{x}} M_{1} … M_{i−1} M_{i+1} … M_{n}). However, most of the those arguments, which at compile time are variables, will be instantiated at run-time: therefore it would be incorrect to compute their complement as empty. Since we cannot foresee this instantiation, we achieve term complementation via the introduction of disequations. This is achieved by the judgment

1.8. CLAUSE COMPLEMENTATION  43

\frac{Notα ⊥}{Γ ⊢ Notα(⊥) = ⊤}

\frac{Notα⊤}{Γ ⊢ Notα(⊤_{q}) = ⋀_{x∈dom(Γ)} ⋀_{xR^{i}q} Not_{x}^{i}(⊤_{q})}

Not_{G}(G) = G′

Notα ←

Γ ⊢ Notα(q ← G) = ( ⋀_{x∈dom(Γ)} ⋀_{xR^{i}q} Not_{x}^{i}(q)) ∧ (¬q ← G′)

Γ ⊢ Notα(D) = D′

Notα∀
Γ ⊢ Notα(∀x:A. D) = ∀x:A. D′

Γ ⊢ Notα(D_{1}) = D′_{1} Γ ⊢ Notα(D_{2}) = D′_{2}

Not∧

Γ ⊢ Notα(D_{1} ∧ D_{2}) = D′_{1} ∨ D′_{2}

Γ ⊢ Notα(D_{1}) = D′_{1} Γ ⊢ Notα(D_{2}) = D′_{2}

Not∨

Γ ⊢ Notα(D_{1} ∨ D_{2}) = D′_{1} ∧ D′_{2}

Σ(q) = A_{1} → ⋯ → A_{n} → prop · ⊢ sh(x, A_{i}) = e_{x}

Not_{x}^{i}⊤

Not_{x}^{i}(⊤_{q}) = ∀Z_{1} :A_{1}…. ∀Z_{n}:A_{n}. ¬q \overline{Z_{e_{x}}^{i}} ← ⊤ Σ(q) = A_{1} → ⋯ → A_{n} → prop · ⊢ sh(x, A_{i}) = e_{x}

Not_{x}^{i}At

Not_{x}^{i}(q \overline{M_{n}}) = ⋀_{1≤j≤n}^{j≠i}(∀Z_{1} :A_{1}…. ∀Z_{n}:A_{n}. ¬q \overline{Z_{e_{x}}^{i}} ← M_{j} ≠^{·} Z_{j})

\frac{e_{x}At}{Γ ⊢ sh(x, a) = x}  \begin{aligned}Γ, y:A ⊢ sh(x, B) = e_{x} \\ & e_{x} →^{y} \\ Γ ⊢ sh(x, A → B) = λy:A. e_{x} \end{aligned}

Figure 1.9: Assumption Complementation: Γ ⊢ Notα(D) = D′ Γ ⊢ Notα(D); note that the latter is type directed and can be see as constraintsbased version of term complementation. We briefly comment on rules Notα⊤ and Notα →:

Draft of February 28, 2000

• Pivot on x:a ∈ Γ.

• Locate a type A_{i} such that x is relevant to Q at i.

• Complement D w.r.t. x and i, by introducing the appropriate disequation.

• Repeat for every relevant x and i.

• Special case: if no x is relevant, the trivial program is returned.

The judgment is not optimized since if M_{j} is essentially existential, an unsatisfiable clause is built; moreover, if it is a ground term, we add a disequation, rather then computing the term complement. We can perform constraint simplification in a separated phase, see Section 1.12.2.

Notice the different treatment of the trivial clause ⊤ by rules Not_{D}⊤ and Notα⊤: if no parameter has been assumed, then ⊤ truly stands for the empty predicate definition and its complement is the universal definition ⊥. If, on the other side Γ is not empty, it means that ⊤_{q} has been introduced during the ⊤-normalization preprocessing phase and has been localized to the predicate q. The rule Not_{x}^{i}⊤ allows to build a new negative assumption w.r.t. q, x, i in case ⊤_{q} is the only dynamic definition of q. As ⊤_{q} carries no information at all concerning q, the most general negative assumption is added. The Γ ⊢ sh(x, A) judgment builds a shallow parameter expression as required by the type of the position in q where it ought to occur; finally, the notation \overline{Z_{e_{x}}^{i}} abridges Z_{1} … Z_{i−1} e_{x} Z_{i+1} … Z_{n}, where the Z’s are fresh logic variables.

The other rules for static and dynamic clause complementation simply recur on the program respecting the duality of conjunction and disjunction w.r.t. negation. This a somewhat delicate point and therefore we discuss it in details. Intuitively, negative clauses stemming from the complement of a clause in the definition of a predicate need to be considered simultaneously. In fact, if an goal is unprovable from its definition, then its negation must be provable from the complement of each clause of its definition; symmetrically if it is provable then its negation must be unprovable from the complement of at least one. What we have described coincides the operational semantics of an operator, which works exactly as disjunction. This is arguably at odd with the commonly held goal-oriented interpretation of the sequent calculus as uniform proofs, since case analysis makes the latter incomplete w.r.t. minimal logic (but see [NL95] for ways to incorporate the former in the framework of uniform proofs). First, we remark that the ∨ is available uniquely as a program constructor and can therefore be used only in the focusing phase of deductions;in (Section ??), we will show how to ‘compile away’ all occurrences of ∨ in clauses. This is an higher-order equivalent of the intersection operator ‘@’ described in [BMPT90]. This will restore completeness of uniform proofs

1.8. CLAUSE COMPLEMENTATION  45
\frac{Not_{G}⊤}{Not_{G}(⊤) =⊥}
\frac{Not_{G} ⊥}{Not_{G}(⊥) = ⊤}

\frac{Not =^{·}}{Not_{G}(M⃗ =^{·} N⃗) = (M⃗ ≠^{·} N⃗)}

\frac{Not ≠^{·}}{Not_{G}(M⃗ ≠^{·} N⃗) = (M⃗ =^{·} N⃗)}

\frac{Not_{G}At}{Not_{G}(Q) = ¬Q}

Not_{G}(G) = G′

Not_{G}∀
Not_{G}(∀x:A. G) = ∀x:A. G′

Not_{G}(G_{1}) = G′_{1} Not_{G}(G_{2}) = G′_{2}

Not∧

Not_{G}(G_{1} ∧ G_{2}) = G′_{1} ∨ G′_{2}

Not_{G}(G_{1}) = G′_{1} Not_{G}(G_{2}) = G′_{2}

Not∨

Not_{G}(G_{1} ∨ G_{2}) = G′_{1} ∧ G′_{2}
Not_{G}(G) = G′

Not_{G} →

Not_{G}(D → G) = D → G′

Figure 1.10: Goal Complementation: Not_{G}(G) = G′

Draft of February 28, 2000

Goal complemenation, that is the judgment Not_{G}(G) depicted in Figure 1.10, only brings the body into a normalized format; namely, in what we may call parametric negation normal form, to stress the distinction from classical negation normal form or even from negation normal form in constructive logics as extension of intuitionism with strong negation [Nel49]. This re-iterates the problem with strong negation we have hinted in Section 1.2; negation is pushed inward but jumps over parametric-hypothetical judgments to respect the operational interpretation of unprovability.

As a final remark, we note that we must take the complementation of a program, seen as a conjunction, predicate definition-wise rather that clause-wise. In fact, it would be incorrect to simply negate a program as it would introduce disjunctions rather than conjunction among predicate definitions. The same remark applies to the ‘dynamic’ program D. Formally, fixed a signature Σ_{P} and given a program P:

Not_{D}(P) = ⋀_{q∈Σ_{P}} Not_{D}(def(q, P))

Similarly for a conjunction of dynamic assumptions D:

Notα(D) = ⋀_{q∈Σ_{P}} Notα(def(q, D))

We abbreviate Not_{D}(def(q)) in def(¬q).

The following example is somehow a special case of the general procedure, as assumption complementation is trivial, but it is useful to clarify in isolation the rules for clause and goal complementation. We refer to the next Section (1.9) for more complex examples.

Example 1.20 An λ-expression is closed if it has no occurrence of free variables; let z:exp be a constant:

cloz : closed z.
clolam : ∀E:exp. closed (lam E) ← (∀x:exp. (closed x → closed (E x).)
cloapp : ∀E_{1} :exp. ∀E_{2} :exp. closed (app E_{1} E_{2}) ← closed E_{1} ∧ closed E_{2}.

Now, def(closed) = cloz ∧ clolam ∧ cloapp. Therefore:

def(¬closed) = Not_{D}(cloz) ⊗ Not_{D}(clolam) ⊗ Not_{D}(cloapp)
Not_{D}(cloz) = ∀( ⋀_{N∈Not(z)} ¬closed N)
= ∀F:exp. ¬closed (lam F) ∧ ∀F_{1}, F_{2} :exp. ¬closed (app F_{1} F_{2}).
Not_{D}(clolam) = ∀(  ⋀_{N∈Not(lam E)} ¬closed N) ∧

∀E:exp. ¬closed (lam E) ← Not_{G}(∀x:exp. (closed x → closed (E x))

= ¬closed z ∧ ∀F_{1}, F_{2} :exp. ¬closed (app F_{1} F_{2}) ∧

∀E:exp. ¬closed (lam E) ← (∀x:exp. (closed x → ¬closed (E x)).

Not_{D}(cloapp) = ∀(  ⋀_{N∈Not(app E_{1}E_{2}))} ¬closed N) ∧

∀E_{1}, E_{2} :exp. ¬closed (app E_{1}E_{2}) ← Not_{G}(closed E_{1} ∧ closed E_{2})

= ¬closed z ∧ ∀F:exp. ¬closed(lam F) ∧

∀E_{1}, E_{2} :exp. ¬closed (app E_{1}E_{2}) ← ¬closed E_{1} ∨ ¬closed E_{2}.

If you want to see the definition simplified, please skip to Example 1.29 and the final result in Example 1.33.

1.9 Augmentation

Now that we have discussed how to perform clause, assumption and goal complementation, we synchronize it together in a phase we call augmentation, which simply insert the correct assumption complementation in a goal and in turn in a clause. We give one judgment to augment a program, aug_{D}(D), which merely recurs on the structure of clauses until it calls goal augmentation, Γ; D ⊢ aug_{G}(G). The latter traverses a goal collecting parameters in Γ and assumptions in D. When it reaches an atom, either it stops, as no parameter has been introduced, or it passes Γ, D to assumption complementation. Some examples will make the whole process clear:

\begin{aligned}X ∈ \{⊤, ⊥\} \\ & aug_{D}X \\ aug_{D}(X) = X \end{aligned}

aug_{D}(D_{1}) = D_{1}^{a} aug_{D}(D_{2}) = D_{2}^{a} aug_{D}∧

aug_{D}(D_{1} ∧ D_{2}) = D_{1}^{a} ∧ D_{2}^{a}

aug_{D}(D_{1}) = D_{1}^{a} aug_{D}(D_{2}) = D_{2}^{a} aug_{D}∨

aug_{D}(D_{1} ∨ D_{2}) = D_{1}^{a} ∨ D_{2}^{a}

aug_{D}([u/x]D) = [u/x]D^{a}
aug_{D}∀^{u}
aug_{D}(∀x:a. D) = ∀x:a. D^{a}

aug_{D}(D) = D^{a} ·; ⊤ ⊢ aug_{G}(G) = G_{a} aug_{D} ←

aug_{D}(D ← G) = D^{a} ← G_{a}

Figure 1.11: Clause Augmentation: aug_{D}(D) = D^{a} X ∈ {⊤, ⊥} or (dis)eq

aug_{G}X

Γ; D ⊢ aug_{G}(X) = X

\frac{aug_{G}At^{⊤}}{·; ⊤ ⊢ aug_{G}(Q) = Q}

Γ ⊢ Notα(D) = D_{¬}

aug_{G}At

Γ; D ⊢ aug_{G}(Q) = D_{¬} → Q

Γ; (D ∧ D) ⊢ aug_{G}(G) = G^{a} aug_{G} →

Γ; D ⊢ aug_{G}(D → G) = D → G^{a} (Γ, y:A); D ⊢ aug_{G}([y/x]G) = [y/x]G^{a}

aug_{G}∀^{y}

Γ; D ⊢ aug_{G}(∀x:a. G) = ∀x:a. G^{a} Γ; D ⊢ aug_{G}([u/x]G) = [u/x]G^{a}

aug_{G}∃^{u}

Γ; D ⊢ aug_{G}(∃x:A. G) = ∃x:A. G^{a}

Γ; D ⊢ aug_{G}(G_{1}) = G_{1}^{a} Γ; D ⊢ aug_{G}(G_{2}) = G_{2}^{a} aug_{G}∧

Γ; D ⊢ aug_{G}(G_{1} ∧ G_{2}) = G_{1}^{a} ∧ G_{2}^{a}

Γ; D ⊢ aug_{G}(G_{1}) = G_{1}^{a} Γ; D ⊢ aug_{G}(G_{2}) = G_{2}^{a} aug_{G}∨

Γ; D ⊢ aug_{G}(G_{1} ∨ G_{2}) = G_{1}^{a} ∨ G_{2}^{a}

Figure 1.12: Goal Augmentation: Γ; D ⊢ aug_{G}(G) = G_{a} Example 1.21 Consider the copy program on λ-terms:

cpapp : ∀E_{1}, E_{2}, F_{1}, F_{2} :exp.
copy (app E_{1}E_{2}) (app F_{1}F_{2})
← copy E_{1} F_{1}
← copy E_{2} F_{2}.
cplam : ∀E:exp → exp. ∀F:exp → exp.
copy (lam E) (lam F)
← (∀x:exp. copy x x
→ copy (E x) (F x)).

The augmentation procedure aug_{D}(cplam) yields aug_{G}(∀x : exp. copy x x → copy (E x) (F x)), which collects x:exp; copy x x and calls x:exp ⊢ Notα(copy x x).

First Not_{1}^{x}(copy x x) = (∀E′:exp. ¬copy E′ x ← x ≠^{·} E′), secondly Not_{2}^{x}(copy x x) =

(∀F′:exp. ¬copy x F′ ← x ≠^{·} F′), yielding:

aug_{D}(cplam) : ∀E:exp → exp. ∀F:exp → exp.
copy (lam E) (lam F)
← (∀x:exp.

(∀E′:exp. ¬copy E′ x ← x ≠^{·} E′) ∧

(∀F′:exp. ¬copy x F′ ← x ≠^{·} F′) →

copy x x → copy (E x) (F x)).

while of course, aug_{D}(cpapp) = cpapp, as enforced by aug_{G}At⊤. If we had a two-parameter version of copy, i.e.

cplam′ : ∀E:exp → exp. ∀F:exp → exp.
copy′ (lam E) (lam F)
← (∀x:exp. ∀y:exp. (copy′ x y)
→ copy′ (E x) (F y)).

Then we would get four calls, namely to:

Not_{1}^{x}(copy′ x y) = (∀E′:exp. ¬copy′ x E′ ← x ≠^{·} E′)
Not_{2}^{x}(copy′ x y) = (∀E′′:exp. ¬copy′ E′′ x ← x ≠^{·} E′′)
Not_{1}^{y}(copy′ x y) = (∀F′:exp. ¬copy′ x F′ ← y ≠^{·} F′)
Not_{2}^{y}(copy′ x y) = (∀F′′:exp. ¬copy′ F′′ y ← y ≠^{·} F′′)

yielding the augmented clause:

aug_{D}(cplam′) : ∀E:exp → exp. ∀F:exp → exp.

copy′ (lam E) (lam F)

← (∀x:exp. ∀x:exp.

(∀E′:exp. ¬copy′ E′ x ← x ≠^{·} E′) ∧

(∀E′′:exp. ¬copy′ x E′′ ← x ≠^{·} E′) ∧

(∀F′:exp. ¬copy′ x F′ ← x ≠^{·} F′) ∧

(∀F′′:exp. ¬copy′ F′′ y ← y ≠^{·} F′′) →

copy′ x y → copy′ (E x) (F y)).

Note that by static analysis of copy', we know that x will never end up in the second argument of copy' and symmetrically this applies to y, too. Thus the call to Not_{2}^{x}, Not_{1}^{y} are useless; however since this kind of data flow analysis is in general undecidable, the augmentation procedure inserts the negation of a clause for every position relevant to the pivot parameter.

Take the typing clause for lambda terms:

oflam : ∀E:exp → exp. ∀T 1, T 2:tp.
of lam(E) arrow(T 1, T 2)
← (∀x:exp. of x T 1 → of E x T 2).

As T 1 is an input term, the correspondent diseqution is inserted:

aug_{D}(oflam) : ∀E:exp → exp. ∀T 1, T 2:tp.
of lam(E) arrow(T 1, T 2)
← (∀x:exp. of x T 1 →

(∀T:tp. ¬of x T ← T ≠^{·} T 1) →

of (E x) T 2).

Consider now a predicate to perform instantiation of a binding operator (in the pattern fragment):

inlam : ∀E:exp → exp. ∀F:exp.
inst (lam E) F
← (∀x:exp. (∀H:exp. copy x H)
→ copy (E x) F).

The call to x:exp ⊢ Notα(∀H:exp. copy x H) leads to Not_{x}^{1}(∀H:exp. copy x H), which yields the unsatisfiable clause ∀H : exp. ∀Z : exp. ¬copy x Z ← Z ≠^{·} H,

while Not_{x}^{2}(∀H : exp. copy x H) yields ∀Z : exp. ¬copy x Z ← Z ≠^{·} x. The

augmentation will simply to

aug_{D}(inlam) : ∀E:exp → exp. ∀F:exp.
inst (lam E) F

← (∀x:exp. (∀H:exp. copy x H) ∧

(∀Z:exp. ¬copy x Z ← Z ≠^{·} x)

→ copy (E x) F).

Let us see how rule Not_{x}^{i}⊤ enters the picture: recall the ⊤-normalized linx lambda clause:

linxlam : ∀E:exp → exp → exp.
linx (λx . lam(λy . E x y))
← (∀z:exp. ⊤_{linx} → linx (λx . E x z)).

The judgment z:exp; ⊤_{linx} ⊢ aug_{G}(linx E x z) triggers the rule Not_{x}^{i}⊤; in turn · ⊢ sh(z, exp → exp) = λy . z and thus Not_{1}^{z}(⊤_{linx}) = ¬linx (λx . z):

aug_{D}(linxlam) : ∀E:exp → exp → exp.
linx (λx . lam(λy . E x y))

← (∀z:exp. ¬linx (λx . z) → linx (λx . E x z)).

We prove that augmented clauses and goals satisfy the augmented schema, where we define Γ; aug_{D}(D) as Γ; D ∧ ¬D, for Γ ⊢ Notα(D) = ¬D and

\frac{aug∘}{aug(∘) = ∘}

aug(S) = S^{a} aug_{D}(D) = D^{a}
aug∥
aug(S∥(Γ; SOME Φ .D)) = S^{a}∥(Γ; SOME Φ .D^{a})

Now, the usual lemma on schema membership:

Lemma 1.22 If Γ; D ∈ S then Γ; aug_{D}(D) ∈ aug(S).

Proof: By induction on the structure of π :: Γ; D ∈ S.

Case

π = (Γ′; D′) ≡_{α} (Γ; θD) ∈_{1} (Γ′; D′) ∈ S∥(Γ; SOME Φ .D)

Γ′; D′ ≡_{α} Γ; θD  By subderivation
Γ′; aug_{D}(D′) ≡_{α} Γ; θ aug_{D}(D)  By definition
Γ′; aug_{D}(D′) ∈ aug(S)∥Γ; SOME Φ .aug_{D}(D)  By rule ∈_{1}
Γ′; aug_{D}(D′) ∈ aug(S∥Γ; SOME Φ .D)  By rule aug∥

Case π ends in ∈_{2}: by IH.

□

We use ⊧_{S^{a}} aug_{D}(D) for ⊢ aug_{D}(D) = D_{a} and ⊧_{S^{a}} D^{a}; analogously for aug_{G}(G).

Lemma 1.23 (Schema Augmentation) Let Γ; D < S and aug(S) = S^{a}. Then:

1. If ⊧_{S} D, then ⊧_{S^{a}} aug_{D}(D).

2. If Γ; D \ G < S, then Γ; D \ aug_{G}(G) < S^{a}.

3. If Γ; D < S then Γ; aug_{D}(D) < S^{a}. Proof: By mutual induction on the structure of π :: ⊧_{S} D, γ :: Γ; D \ G < S and σ :: Γ; D < S. We show the crucial cases: Case

π = \begin{aligned}X ∈ \{Q, ⊤, ⊥\} \\ & ⊧_{S} X \\ ⊧_{S} X \end{aligned}

Immediately Γ; D ⊢ aug_{D}(X) = X and

π′ = \begin{aligned}X ∈ \{Q, ⊤, ⊥\} \\ & ⊧_{S} X \\ ⊧_{S^{a}} X \end{aligned}

Case

π = \begin{aligned}⊧_{S} D ·; ⊤ \ G < S \\ & ⊧_{S}→ \\ ⊧_{S} G → D \end{aligned}

⊧_{S} D  By subderivation
⊧_{S^{a}} aug_{D}(D)  By IH 1
·; ⊤ \ G < S  By subderivation
·; ⊤ \ aug_{G}(G) < S^{a}  By IH 2
⊧_{S^{a}} aug_{G}(G) → aug_{D}(D)  By rule ⊧_{S}→
⊧_{S^{a}} aug_{D}(G → D)  By rule aug_{D} →

Case

γ = X ∈ {⊤, ⊥} or (dis)eq Γ; D < S \X Γ; D \ X < S
Γ; D < S  By subderivation
Γ; aug_{D}(D) < S^{a}  By IH 3
Γ; D ⊢ aug_{G}(X) = X  By rule aug_{G}X
Γ; aug_{D}(D) \ X < S^{a}  By rule \X

Case

γ = \begin{aligned}Γ; D < S \\ & \At \\ Γ; D \ Q < S \end{aligned}

Subcase ·; ⊤ < S  By subderivation
·; ⊤ < S^{a}  By rule <_{1}
·; ⊤ ⊢ Q < S^{a}  By rule aug_{G}At⊤
·; ⊤ \ aug_{G}(Q) < S^{a}  By rule \At

Draft of February 28, 2000

Subcase Γ; D < S  By subderivation
Γ; aug_{D}(D) < S^{a}  By IH 3
Γ; aug_{D}(D) \ Q < S^{a}  By rule \Q
Γ; D ∧ Notα(D) \ Q < S^{a}  By def. of aug_{D}(D)
Γ; D \ Notα(D) → Q < S^{a}  By rule aug_{G}At
Γ; D \ aug_{G}(Q) < S^{a}  By rule \ →

Case

γ = \begin{aligned}⊧_{S} D Γ; D ∧ D \ G < S \\ & \ → \\ Γ; D \ D → G < S \end{aligned}

⊧_{S} D  By subderivation
⊧_{S^{a}} aug_{D}(D)  By IH 1
Γ; D ∧ D \ G < S  By subderivation
Γ; D ∧ D \ aug_{G}(G) < S^{a}  By IH 2
Γ; D \ D → aug_{G}(G) < S^{a}  By rule \ →
Γ; D \ aug_{G}(D → G) < S^{a}  By rule aug_{G} →

Case

σ = \frac{<_{1}}{·; ⊤ < S}

Then immediately:

σ′ = \frac{<_{1}}{·; ⊤ < S^{a}}

Case

σ = \begin{aligned}(Γ′; D′) ∈ S ⊧_{S} D′ (Γ; D) < S \\ & <_{2} \\ (Γ, ⌈Γ′⌉); (D ∧ ⌈D′⌉) < S \end{aligned}

Γ; D < S  By subderivation
Γ; aug_{D}(D) < S^{a}  By IH 3
Γ′; D′ ∈ S  By subderivation
Γ′; aug_{D}(D′) ∈ S^{a}  By Lemma 1.22
⊧_{S} D′  By subderivation
⊧_{S^{a}} aug_{D}(D′)  By IH 1
(Γ, ⌈Γ′⌉); aug_{D}(D) ∧ aug_{D}(⌈D′)⌉) < S^{a}  By rule <_{2}
(Γ, ⌈Γ′⌉); aug_{D}(D ∧ ⌈D′⌉) < S^{a}  By rule aug_{D}∧
□

Lemma 1.24 If M⃗ is a simple term, then ⊧_{S^{a}} ⋀_{N⃗∈Not(M⃗)} ∀(¬(q N⃗) ← ⊤).

Proof: By rules ⊧_{S^{a}} ∧, ⊧_{S} ∀, ⊧_{S^{a}}→, \⊤, ⊧_{S} At, \At. □

The following Lemma ensures that augmented clauses are closed under negation. In particular, for Γ; D < S^{a}, if D ∈ D, so is Γ ⊢ Notα(D). We use Γ; D \ Not_{G}(G) < S^{a} for Not_{G}(G) = G_{¬} and Γ; D \ G_{¬} < S^{a}. Similarly for Not_{D}(D).

Lemma 1.25 (Negative Schema Augmentation) Let Γ; D < S^{a}. Then: 1. If ⊧_{S^{a}} aug_{D}(D), then ⊧_{S^{a}} Not_{D}(aug_{D}(D)).

2. If Γ; D \ aug_{G}(G) < S^{a}, then Γ; D \ Not_{G}(aug_{G}(G)) < S^{a}. Proof: By mutual induction on the structure of π :: ⊧_{S^{a}} aug_{D}(D) and γ :: Γ; D \ aug_{G}(G) < S^{a}. Case

π = \frac{⊧_{S^{a}}⊥}{⊧_{S^{a}} aug_{D}(⊥)}

By rule aug_{D}(⊥) =⊥ and ⊢ Not_{D}(⊥) = ⊤: thus

π′ = \frac{⊧_{S^{a}} ⊤}{⊧_{S^{a}} ⊤}

Case

π = \frac{⊧_{S^{a}} ⊤}{⊧_{S^{a}} aug_{D}(⊤)}

By rule aug_{D}(⊤) = ⊤ and ⊢ Not_{D}(⊤) =⊥: thus

π′ = \frac{⊧_{S^{a}}⊥}{⊧_{S^{a}}⊥}

Case π ends in ⊧_{S^{a}} aug_{D}(q M⃗ ← G):

⊧_{S^{a}} aug_{D}(q M⃗) ← aug_{G}(G)  By rule aug_{D} →
⊧_{S^{a}} ¬q M⃗  By rule ⊧_{S^{a}} At
·; ⊤ \ aug_{G}(G) < S^{a}  By rule ⊧_{S}→
·; ⊤ \ Not_{G}(aug_{G}(G)) < S^{a}  By IH 2
⊧_{S^{a}} ¬q M⃗ ← Not_{G}(aug_{G}(G))  By rule ⊧_{S^{a}}→
⊧_{S^{a}} ⋀_{N⃗∈Not(M⃗)} ∀(¬(q N⃗))  By Lemma 1.24

⊧_{S^{a}} ⋀_{N⃗∈Not(M⃗)} ∀(¬(q N⃗) ← ⊤) ∧ (¬q M⃗ ← Not_{G}(aug_{G}(G)))

By rule ⊧_{S^{a}} ∧

⊧_{S^{a}} Not_{D}(q M⃗ ← aug_{G}(G))  By rule aug_{D} →
⊧_{S^{a}} Not_{D}(aug_{D}(q M⃗) ← aug_{G}(G))  By rule Not_{D} →
⊧_{S^{a}} Not_{D}(aug_{D}(q M⃗ ← G))  By rule aug_{D} →

Case π ends in ⊧_{S^{a}} aug_{D}(∀x:a. D):

⊧_{S^{a}} ∀x:a. aug_{D}(D)  By rule aug_{D}∀
⊧_{S^{a}} [u/x]aug_{D}(D)  By rule ⊧_{S^{a}} ∀
⊧_{S^{a}} [u/x]Not_{D}(aug_{D}(D))  By IH 1
⊧_{S^{a}} ∀x:a. Not_{D}(aug_{D}(D))  By rule ⊧_{S^{a}} ∀
⊧_{S^{a}} Not_{D}(∀x:a. aug_{D}(D))  By rule Not_{D}∀
⊧_{S^{a}} Not_{D}(aug_{D}(∀x:a. D))  By rule aug_{D}∀

Draft of February 28, 2000

Case π ends in ⊧_{S^{a}} aug_{D}(D_{1} ∧ D_{2}):

⊧_{S^{a}} aug_{D}(D_{1}) ∧ aug_{D}(D_{2})  By rule aug_{D}∧
⊧_{S^{a}} aug_{D}(D_{1}) and ⊧_{S^{a}} aug_{D}(D_{2})  By rule ⊧_{S} ∧
⊧_{S^{a}} Not_{D}(aug_{D}(D_{1})) and ⊧_{S^{a}} Not_{D}(aug_{D}(D_{2}))  By IH 1
⊧_{S^{a}} Not_{D}(aug_{D}(D_{1})) ∨ Not_{D}(aug_{D}(D_{2}))  By rule ⊧_{S} ∨
⊧_{S^{a}} Not_{D}(aug_{D}(D_{1}) ∧ aug_{D}(D_{2}))  By rule Not_{D}∧
⊧_{S^{a}} Not_{D}(aug_{D}(D_{1} ∧ D_{2}))  By rule aug_{D}∧

Case π ends in ⊧_{S^{a}} aug_{D}(D_{1} ∨ D_{2}):

⊧_{S^{a}} aug_{D}(D_{1}) ∨ aug_{D}(D_{2})  By rule aug_{D}∨
⊧_{S^{a}} aug_{D}(D_{1}) and ⊧_{S^{a}} aug_{D}(D_{2})  By rule ⊧_{S} ∨
⊧_{S^{a}} Not_{D}(aug_{D}(D_{1})) and ⊧_{S^{a}} Not_{D}(aug_{D}(D_{2}))  By IH 1
⊧_{S^{a}} Not_{D}(aug_{D}(D_{1})) ∧ Not_{D}(aug_{D}(D_{2}))  By rule ⊧_{S} ∧
⊧_{S^{a}} Not_{D}(aug_{D}(D_{1}) ∨ aug_{D}(D_{2}))  By rule Not_{D}∨
⊧_{S^{a}} Not_{D}(aug_{D}(D_{1} ∨ D_{2}))  By rule aug_{D}∨

Case γ ends in Γ; D \ aug_{G}(⊤) < S^{a}:

Γ; D \ ⊤ < S^{a}  By rule aug_{G}⊤
Γ; D < S^{a}  By subderivation
Γ; D ⊢ Not_{G}(⊤) =⊥  By rule Not_{G}⊤
Γ; D\ ⊥< S^{a}  By rule \ ⊥

Case γ ends in Γ; D \ aug_{G}(⊥) < S^{a}:

Γ; D\ ⊥< S^{a}  By rule aug_{G} ⊥
Γ; D < S^{a}  By subderivation
Γ; D ⊢ Not_{G}(⊥) = ⊤  By rule Not_{G} ⊥
Γ; D \ ⊤ < S^{a}  By rule \ ⊥

Case γ ends in Γ; D \ aug_{G}(M⃗ =^{·} N⃗) < S^{a}:

Γ; D \ M⃗ =^{·} N⃗ < S^{a}  By rule aug_{G} =^{·}
Γ; D < S^{a}  By subderivation
Γ; D ⊢ Not_{G}(M⃗ =^{·} N⃗) = (M⃗ ≠^{·} N⃗)  By rule Not_{G} =^{·}
Γ; D \ M⃗ ≠^{·} N⃗ < S^{a}  By rule \ ≠^{·}

Case γ ends in Γ; D \ aug_{G}(M⃗ ≠^{·} N⃗) < S^{a}:

Γ; D \ M⃗ ≠^{·} N⃗ < S^{a}  By rule aug_{G} ≠^{·}
Γ; D < S^{a}  By subderivation
Γ; D ⊢ Not_{G}(M⃗ ≠^{·} N⃗) = (M⃗ =^{·} N⃗)  By rule Not_{G} ≠^{·}
Γ; D \ M⃗ =^{·} N⃗ < S^{a}  By rule \ ≠^{·}

Case γ ends in Γ; D \ aug_{G}(Q) < S^{a}:

Subcase ·; ⊤ \ Q < S^{a}  By rule aug_{G}At⊤
·; ⊤ < S^{a}  By subderivation
·; ⊤ \ ¬Q < S^{a}  By rule Not_{G}At
·; ⊤ \ Not_{G}(Q) < S^{a}  By rule Not_{G} →
·; ⊤ \ Not_{G}(aug_{G}(Q)) < S^{a}  By rule aug_{G}At⊤
Subcase Γ; D \ Notα(D) → Q < S^{a}  By rule aug_{G}At
Γ; (D ∧ Notα(D)) \ Q < S^{a}  By rule \ →
Γ; (D ∧ Notα(D)) < S^{a}  By subderivation
Γ; (D ∧ Notα(D)) \ ¬Q < S^{a}  By rule \At
Γ; D \ Notα(D) → ¬Q < S^{a}  By rule \ →
Γ; D \ Notα(D) → Not_{G}(Q) < S^{a}  By rule Not_{G}At
Γ; D \ Not_{G}(Notα(D) → Q) < S^{a}  By rule Not_{G} →
Γ; D \ Not_{G}(aug_{G}(Q)) < S^{a}  By rule aug_{G}At

Case γ ends in Γ; D \ aug_{G}(D → G) < S^{a}:

Γ; D \ aug_{D}(D) → aug_{G}(G) < S^{a}  By rule aug_{G} →
⊧_{S^{a}} aug_{D}(D) and Γ; (D ∧ D) \ aug_{G}(G) < S^{a}  By rule \ →
Γ; (D ∧ aug_{D}(D)) \ Not_{G}(aug_{G}(G)) < S^{a}  By IH 2
Γ; D \ aug_{D}(D) → Not_{G}(aug_{G}(G)) < S^{a}  By rule \ →
Γ; D \ Not_{G}(aug_{D}(D) → aug_{G}(G)) < S^{a}  By rule Not_{G} →
Γ; D \ Not_{G}(aug_{G}(D → G)) < S^{a}  By rule aug_{G} →

Case γ ends in Γ; D \ aug_{G}(∀x:a. G) < S^{a}:

Γ; D \ ∀x:a. aug_{G}(G) < S^{a}  By rule aug_{G}∀
(Γ, y:A); D \ [y/x]aug_{G}(G) < S^{a}  By rule \∀
(Γ, y:A); D \ [y/x]Not_{G}(aug_{G}(G)) < S^{a}  By IH 2
Γ; D \ ∀x:a. Not_{G}(aug_{G}(G)) < S^{a}  By rule \∀
Γ; D \ Not_{G}(∀x:a. aug_{G}(G)) < S^{a}  By rule Not_{G}∀
Γ; D \ Not_{G}(aug_{G}(∀x:a. G)) < S^{a}  By rule aug_{G}∀

Case γ ends in Γ; D \ aug_{G}(G_{1} ∨ G_{2}) < S^{a}:

Γ; D \ aug_{G}(G_{1}) ∨ aug_{G}(G_{2}) < S^{a}  By rule aug_{G}∨
Γ; D \ aug_{G}(G_{1}) < S^{a} and Γ; D \ aug_{G}(G_{2}) < S^{a}  By rule \∨
Γ; D \ Not_{G}(aug_{G}(G_{1})) < S^{a} and Γ; D \ Not_{G}(aug_{G}(G_{2})) < S^{a} By IH 2
Γ; D \ Not_{G}(aug_{G}(G_{1})) ∧ Not_{G}(aug_{G}(G_{2}) < S^{a}  By rule \∧
Γ; D \ Not_{G}(aug_{G}(G_{1}) ∨ aug_{G}(G_{2})) < S^{a}  By rule Not_{G}∨
Γ; D \ Not_{G}(aug_{G}(G_{1} ∨ G_{2})) < S^{a}  By rule aug_{G}∨

Case γ ends in Γ; D \ aug_{G}(G_{1} ∧ G_{2}) < S^{a}:

Γ; D \ aug_{G}(G_{1}) ∧ aug_{G}(G_{2}) < S^{a}  By rule aug_{G}∧
Γ; D \ aug_{G}(G_{1}) < S^{a} and Γ; D \ aug_{G}(G_{2}) < S^{a}  By rule \∧
Γ; D \ Not_{G}(aug_{G}(G_{1})) < S^{a} and Γ; D \ Not_{G}(aug_{G}(G_{2})) < S^{a} By IH 2
Γ; D \ Not_{G}(aug_{G}(G_{1})) ∨ Not_{G}(aug_{G}(G_{2}) < S^{a}  By rule \∨
Γ; D \ Not_{G}(aug_{G}(G_{1}) ∧ aug_{G}(G_{2})) < S^{a}  By rule Not_{G}∧
Γ; D \ Not_{G}(aug_{G}(G_{1} ∧ G_{2})) < S^{a}  By rule aug_{G}∧

□

We can combine the two latter lemmata 1.23 and 1.25 to prove that augmentation guarantees that static and dynamic clauses are closed under complementation.

Corollary 1.26 (Closure under Complementation) If ⊧_{S} D, then ⊧_{S^{a}} Not_{D}(aug_{D}(D)).

1.10 Exclusivity

We use Γ; D ⊢_{P} Not_{G}(G) for Not_{G}(G) = G′ and Γ; D ⊢_{P} G′; Γ; D ⊢_{P} Not_{D}(D)>>¬Q for Not_{D}(D) = D′ and Γ; D ⊢_{P} D′>>¬Q; similarly for Notα. Recall that D ∈ def(q, P ∧ D) denotes that D is a top-level conjunct in the static or dynamic definition of q. Similarly, D ∈ def(¬q, P ∧D) denotes that D is a top-level disjunct in the static or dynamic definition of ¬q.

Theorem 1.27 (Exclusivity) Let aug_{D}(P) ⟹^{D} S^{a} and Γ; D < S^{a}. It is not the case that both Γ; D ⊢_{P} G and Γ; D ⊢_{P} Not_{G}(G).

Proof: We generalize this to; let D ∈ def(q, P ∧ D):

1. It is not the case that there is S^{+} :: Γ; D ⊢_{P} G and there is S^{−} :: Γ; D ⊢_{P} Not_{G}(G).

2. It is not the case that I^{+} :: Γ; D ⊢_{P} D>>Q and I^{−} :: Γ; D ⊢_{P} D′>>Not_{G}(Q), for all D′ ∈ def(¬q, P ∧ D).

We proceed by mutual induction on the structure of I^{+} and S^{+}, by assuming the existence of the latter. Note that immediately Not_{G}(Q) = ¬Q. Moreover, the negative definition implies an atom iff so does every disjunct; thus it will suffice to show absurdity for one of the latter. The second statement thus unfolds in four distinct cases:

2.1 Let D ∈ def(q, P) It is not the case that: I^{+} :: Γ; D ⊢_{P} D>>Q and I^{−} :: Γ; D ⊢_{P} Not_{D}(D)>>¬Q.

Case

I^{+} = \frac{>> ⊥}{Γ; D ⊢_{P}⊥ >>Q}

But there can be no proof of ¬Q from Not_{D}(⊥) = ⊤.

Draft of February 28, 2000

Case

I^{+} = \begin{aligned}Γ; D ⊢_{P} \overline{N_{n}} =^{·} \overline{M_{n}} Γ; D ⊢_{P} G \\ & >> → \\ Γ; D ⊢_{P} (q \overline{N_{n}} ← G)>>q \overline{M_{n}} \end{aligned}

and I^{−} ends in Γ; D ⊢_{P} Not_{D}(q \overline{N_{n}} ← G)>>¬q \overline{M_{n}}:

Γ; D ⊢_{P} \overline{N_{n}} =^{·} \overline{M_{n}}  By subderivation
· ⊢ \overline{M_{n}} ∈ ∥\overline{N_{n}}∥ (∗)  By def. of ∥ ∥
S_{1}^{+} :: Γ; D ⊢_{P} G  By subderivation

Γ; D ⊢_{P} ⋀_{\overline{S_{n}}∈Not(\overline{N_{n}})} ∀(¬q \overline{S_{n}} ← ⊤) ∧ ¬q \overline{N_{n}} ← Not_{G}(G)>>¬q \overline{M_{n}}

By rule Not_{D} →

Subcase Γ; D ⊢_{P} ⋀_{\overline{S_{n}}∈Not(\overline{N_{n}})} ∀(¬q \overline{S_{n}} ← ⊤)>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} ∀(¬q \overline{S_{n}} ← ⊤)>>¬q \overline{M_{n}} for some \overline{S_{n}}  By inversion
Γ; D ⊢_{P} [σ](¬q \overline{S_{n}}) ← ⊤>>¬q \overline{M_{n}} for some σ  By inversion
Γ; D ⊢_{P} [σ]\overline{S_{n}} =^{·} \overline{M_{n}}  By inversion
· ⊢ \overline{M_{n}} ∈ ∥Not(\overline{N_{n}})∥  By definition of ∥ ∥
⊥  By term exclusivity with (∗)
Subcase Γ; D ⊢_{P} ¬q \overline{N_{n}} ← Not_{G}(G)>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} Not_{G}(G)  By inversion
⊥  By IH 1 w.r.t. S_{1}^{+}

Case

I^{+} = \begin{aligned}Γ; D ⊢_{P} D_{1}>>Q Γ; D ⊢_{P} D_{2}>>Q \\ & >>∨ \\ Γ; D ⊢_{P} (D_{1} ∨ D_{2})>>Q \end{aligned}

and I^{−} ends in Γ; D ⊢_{P} Not_{D}(D_{1} ∨ D_{2})>>¬Q:

Γ; D ⊢_{P} D_{1}>>Q  By subderivation
Γ; D ⊢_{P} D_{2}>>Q  By subderivation
Γ; D ⊢_{P} Not_{D}(D_{1}) ∧ Not_{D}(D_{2})>>¬Q  By rule Not_{D}∨
Subcase Γ; D ⊢_{P} Not_{D}(D_{1})>>¬Q  By inversion
⊥  By IH 2.1
Subcase Γ; D ⊢_{P} Not_{D}(D_{2})>>¬Q  By inversion
⊥  By IH 2.1

Case

I^{+} = \begin{aligned}Γ; D ⊢_{P} D_{1}>>Q \\ & >>∧ \\ Γ; D ⊢_{P} (D_{1} ∧ D_{2})>>Q \end{aligned}

and I^{−} ends in Γ; D ⊢_{P} Not_{D}(D_{1} ∧ D_{2})>>¬Q:

Γ; D ⊢_{P} D_{1}>>Q  By subderivation
Γ; D ⊢_{P} Not_{D}(D_{1}) ∨ Not_{D}(D_{2})>>¬Q  By rule Not_{D}∧
Γ; D ⊢_{P} Not_{D}(D_{1})  By inversion
⊥  By IH 2.1

Case

I^{+} = \begin{aligned}Γ; D ⊢_{P} D_{2}>>Q \\ & >>∧ \\ Γ; D ⊢_{P} (D_{1} ∧ D_{2})>>Q \end{aligned}

and I^{−} ends in Γ; D ⊢_{P} Not_{D}(D_{1} ∧ D_{2})>>¬Q:

Γ; D ⊢_{P} D_{2}>>Q  By inversion
Γ; D ⊢_{P} Not_{D}(D_{1}) ∨ Not_{D}(D_{2})>>¬Q  By rule Not_{D}∧
Γ; D ⊢_{P} Not_{D}(D_{2})>>¬Q  By inversion
⊥  By IH 2.1

Case

I^{+} = \begin{aligned}Γ ⊢ t : A Γ; D ⊢_{P} [t/x]D>>Q \\ & >>∀ \\ Γ; D ⊢_{P} ∀x:A. D>>Q \end{aligned}

and I^{−} ends in Γ; D ⊢_{P} Not_{D}(∀x:A. D)>>¬Q:

Γ; D ⊢_{P} [t/x]D>>Q  By subderivation
Γ; D ⊢_{P} ∀x:A. Not_{D}(D)>>¬Q  By rule Not_{D}∀
Γ; D ⊢_{P} [t/x]Not_{D}(D)>>¬Q  By inversion
⊥  By IH 2.1

2.2 Let D ∈ def(q, P) and D′ ∈ def(¬q, D). It is not the case that I^{+} :: Γ; D ⊢_{P} D>>Q and I^{−} :: Γ; D ⊢_{P} >>D′¬Q.

Case

I^{+} = \frac{>>At}{Γ; D ⊢_{P}⊥ >>Q}

But there can be no proof of ¬Q from Notα(⊥) = ⊤.

Case

I^{+} = \begin{aligned}Γ; D ⊢_{P} \overline{S_{n}} =^{·} \overline{M_{n}} Γ; D ⊢_{P} G \\ & >> → \\ Γ; D ⊢_{P} (q \overline{S_{n}} ← G)>>q \overline{M_{n}} \end{aligned}

and I^{−} ends in Γ; D ⊢_{P} Notα(q \overline{N_{e_{x}}^{i}} ← H)>>¬q \overline{M_{n}}, where q \overline{N_{e_{x}}^{i}} ← H ∈ def(q, D).

Γ; D ⊢_{P} \overline{S_{n}} =^{·} \overline{M_{n}}  By subderivation
Γ; D ⊢_{P} S_{i} =^{·} M_{i} 1 ≤ i ≤ n (∗)  By subderivation

Γ; D ⊢_{P} ⋀_{x∈dom(Γ)} ⋀_{xR^{i}q} Not_{x}^{i}(q \overline{N_{e_{x}}^{i}}) ∧ (¬q \overline{N_{e_{x}}^{i}} ← Not_{G}(H))>>¬q \overline{M_{n}} By rule Notα →

Subcase Γ; D ⊢_{P} ⋀_{x∈dom(Γ)} ⋀_{xR^{i}q} Not_{x}^{i}(q \overline{N_{e_{x}}^{i}})>>¬q \overline{M_{n}} By inversion
Γ; D ⊢_{P} ⋀_{xR^{i}q} Not_{x}^{i}(q \overline{N_{e_{x}}^{i}})>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} Not_{x}^{i}(q \overline{N_{e_{x}}^{i}})>>¬q \overline{M_{n}}  By inversion

Γ; D ⊢_{P} ⋀_{1≤j≤n,j≠i}(∀Z_{1} :A_{1}…. ∀Z_{n}:A_{n}. ¬q \overline{Z_{x}^{i}} ← N_{j} ≠^{·} Z_{j})>>¬q \overline{M_{n}}

By rule Not_{x}^{i} →

Γ; D ⊢_{P} ∀Z_{1} :A_{1}…. ∀Z_{n}:A_{n}. ¬q \overline{Z_{e_{x}}^{i}} ← N_{j} ≠^{·} Z_{j}>>¬q \overline{M_{n}}By inv.

Γ; D ⊢_{P} [σ]\overline{Z_{e_{x}}^{i}} =^{·} \overline{M_{n}}  By inv. and x ∉ dom(σ)
Γ; D ⊢_{P} e_{x} =^{·} M_{i}  By inversion
⊥  From above line (∗) and constructor restriction on S_{i}
Subcase Γ; D ⊢_{P} ¬q \overline{N_{e_{x}}^{i}} ← Not_{G}(H)>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} \overline{N_{e_{x}}^{i}} =^{·} \overline{M_{n}}  By inversion
Γ; D ⊢_{P} e_{x} =^{·} M_{i}  By inversion
⊥  From above line (∗) and constructor restriction on S_{i}

Case

I^{+} = \begin{aligned}Γ; D ⊢_{P} D_{1}>>Q Γ; D ⊢_{P} D_{2}>>Q \\ & >>∨ \\ Γ; D ⊢_{P} (D_{1} ∨ D_{2})>>Q \end{aligned}

and I^{−} ends in Γ; D ⊢_{P} Notα(D′_{1} ∨ D′_{2})>>¬Q:

Γ; D ⊢_{P} D_{1}>>Q  By subderivation
Γ; D ⊢_{P} D_{2}>>Q  By subderivation
Γ; D ⊢_{P} Notα(D′_{1}) ∧ Notα(D′_{2})>>¬Q  By rule Notα∨
Subcase Γ; D ⊢_{P} Notα(D′_{1})>>¬Q  By inversion
⊥  By IH 2.2
Subcase Γ; D ⊢_{P} Notα(D′_{2})>>¬Q  By inversion
⊥  By IH 2.2

Case

I^{+} = \begin{aligned}Γ; D ⊢_{P} D_{1}>>Q \\ & >>∧ \\ Γ; D ⊢_{P} (D_{1} ∧ D_{2})>>Q \end{aligned}

and I^{−} ends in Γ; D ⊢_{P} Notα(D′_{1} ∧ D′_{2})>>¬Q:

Γ; D ⊢_{P} D_{1}>>Q  By subderivation
Γ; D ⊢_{P} Notα(D′_{1}) ∨ Notα(D′_{2})>>¬Q  By rule Notα∧
Γ; D ⊢_{P} Notα(D′_{1})  By inversion
⊥  By IH 2.2

Case

I^{+} = \begin{aligned}Γ; D ⊢_{P} D_{2}>>Q \\ & >>∧ \\ Γ; D ⊢_{P} (D_{1} ∧ D_{2})>>Q \end{aligned}

and I^{−} ends in Γ; D ⊢_{P} Notα(D′_{1} ∧ D′_{2})>>¬Q:

Γ; D ⊢_{P} D_{2}>>Q  By inversion
Γ; D ⊢_{P} Notα(D′_{1}) ∨ Notα(D′_{2})>>¬Q  By rule Notα∧
Γ; D ⊢_{P} Notα(D′_{2})>>¬Q  By inversion
⊥  By IH 2.2

Case

I^{+} = \begin{aligned}Γ ⊢ t : A Γ; D ⊢_{P} [t/x]D_{1}>>Q \\ & >>∀ \\ Γ; D ⊢_{P} ∀x:a. D_{1}>>Q \end{aligned}

and I^{−} ends in Γ; D ⊢_{P} Notα(∀x:a. D′)>>¬Q:

Draft of February 28, 2000

Γ; D ⊢_{P} [t/x]D_{1}>>Q  By subderivation
Γ; D ⊢_{P} ∀x:A. Notα(D′)>>¬Q  By rule Notα∀
Γ; D ⊢_{P} [t/x]Notα(D′)>>¬Q  By inversion
⊥  By IH 2.2

2.3 Let D ∈ def(q, D) and D′ ∈ def(¬q, P). It is not the case that I^{+} :: Γ; D ⊢_{P} D>>Q and I^{−} :: Γ; D ⊢_{P} D′>>¬Q. Case

I^{+} = \begin{aligned}Γ; D ⊢_{P} \overline{N_{e_{x}}^{i}} =^{·} \overline{M_{n}} Γ; D ⊢_{P} H \\ & >> → \\ Γ; D ⊢_{P} q \overline{N_{e_{x}}^{i}} ← H>>q \overline{M_{n}} \end{aligned}

and I^{−} ends in Γ; D ⊢_{P} Not_{D}(q \overline{S_{n}} ← G)>>¬q \overline{M_{n}}.

Γ; D ⊢_{P} \overline{N_{e_{x}}^{i}} =^{·} \overline{M_{n}}  By subderivation
Γ; D ⊢_{P} e_{x} =^{·} M_{i} (∗) 1 ≤ i ≤ n  By subderivation

Γ; D ⊢_{P} ⋀_{\overline{T_{n}}∈Not(\overline{S_{n}})} ∀(¬q \overline{T_{n}} ← ⊤) ∧ (¬q \overline{S_{n}} ← Not_{G}(G))>>¬q \overline{M_{n}}

By rule Not_{D} →

Subcase Γ; D ⊢_{P} ⋀_{\overline{T_{n}}∈Not(\overline{S_{n}})} ∀(¬q \overline{T_{n}} ← ⊤)>>q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} ∀(¬q \overline{T_{n}} ← ⊤)>>q \overline{M_{n}} for some \overline{S_{n}}  By inversion
Γ; D ⊢_{P} [σ](¬q \overline{T_{n}}) ← ⊤>>¬q \overline{M_{n}} for some σ  By inversion
Γ; D ⊢_{P} [σ]\overline{T_{n}} =^{·} \overline{M_{n}}  By inversion
Γ; D ⊢_{P} [σ]T_{i} =^{·} M_{i}  By inversion
⊥  Above line, (∗) and eigenvariable condition
Subcase Γ; D ⊢_{P} ¬q \overline{S_{n}} ← Not_{G}(G)>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} \overline{S_{n}} =^{·} \overline{M_{n}}  By inversion
Γ; D ⊢_{P} S_{i} =^{·} M_{i}  By inversion
⊥  From above line (∗) and constructor restriction on S_{i}

Case I^{+} ends in >>∨, >> ∧ >>∀: symmetric to case 2.2. 2.4 Let D ∈ def(q, D) and D′ ∈ def(¬q, D). It is not the case that I^{+} ::

Γ; D ⊢_{P} D>>Q and I^{−} :: Γ; D ⊢_{P} D′>>¬Q. Case

I^{+} = \begin{aligned}Γ; D ⊢_{P} \overline{N_{e_{x}}^{i}} =^{·} \overline{M_{n}} Γ; D ⊢_{P} G \\ & >> → \\ Γ; D ⊢_{P} q \overline{N_{e_{x}}^{i}} ← G>>q \overline{M_{n}} \end{aligned}

and I^{−} ends in Γ; D ⊢_{P} Notα(q \overline{N_{e_{x}}^{i}} ← G)>>¬q \overline{M_{n}}.

S_{1}^{+} :: Γ; D ⊢_{P} G  By subderivation
Γ; D ⊢_{P} \overline{N_{e_{x}}^{i}} =^{·} \overline{M_{n}}  By subderivation
Γ; D ⊢_{P} N_{j} =^{·} M_{j} (+) 1 ≤ i, j ≤ n, i ≠ j  By inversion

Γ; D ⊢_{P} ⋀_{x∈dom(Γ)} ⋀_{xR^{i}q} Not_{x}^{i}(q \overline{N_{e_{x}}^{i}}) ∧ (¬q \overline{N_{e_{x}}^{i}}) ← Not_{G}(G))>>¬q \overline{M_{n}} By rule Notα →

Draft of February 28, 2000

Subcase Γ; D ⊢_{P} ⋀_{x∈dom(Γ)} ⋀_{xR^{i}q} Not_{x}^{i}(q \overline{N_{e_{x}}^{i}})>>¬q \overline{M_{n}} By inversion
Γ; D ⊢_{P} ⋀_{xR^{i}q} Not_{x}^{i}(q\overline{N_{e_{x}}^{i}})>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} Not_{x}^{i}(q \overline{N_{e_{x}}^{i}})>>¬q \overline{M_{n}}  By inversion

Γ; D ⊢_{P} ⋀_{1≤j≤n,j≠i}(∀Z_{1} :A_{1}…. ∀Z_{n}:A_{n}. ¬q \overline{Z_{e_{x}}^{i}} ← Z_{j} ≠^{·} N_{j})>>¬q \overline{M_{n}}

By inversion

Γ; D ⊢_{P} (∀Z_{1} :A_{1}…. ∀Z_{n}:A_{n}. ¬q \overline{Z_{e_{x}}^{i}} ← Z_{j} ≠^{·} N_{j})>>¬q \overline{M_{n}}

By inversion

Γ; D ⊢_{P} [M_{j}/Z_{j}]Z_{j} ≠^{·} N_{j}  By inversion
⊥  Above line and (+)
Subcase Γ; D ⊢_{P} ¬q \overline{N_{e_{x}}^{i}} ← Not_{G}(G)>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} Not_{G}(G)  By inversion
⊥  By IH 1 on S_{1}^{+}

Case I^{+} ends in >>∨, >>∧, >>∀: by IH as in case 2.1 with Notα in place of Not_{D}.

Case

S^{+} = Γ; D ⊢_{P} def(q, P ∧ D)>>Q ⊢ atm Γ; D ⊢_{P} Q

and S^{−} ends in Γ; D ⊢_{P} Not_{G}(Q):

Γ; D ⊢_{P} def(q, P ∧ D)>>Q  By subderivation
Γ; D ⊢_{P} D>>Q for D ∈ def(q, P ∧ D)  By subderivation
Γ; D ⊢_{P} ¬Q  By rule Not_{G}At
Γ; D ⊢_{P} def(¬q, PD)>>¬Q  By inversion
Γ; D ⊢_{P} D′>>¬Q for D′ ∈ def(¬q, P ∧ D)  By inversion
⊥  By IH 2

Case

S^{+} = \begin{aligned}Γ; D ⊢_{P} G_{1} Γ; D ⊢_{P} G_{2} \\ & ⊢ ∧ \\ Γ; D ⊢_{P} G_{1} ∧ G_{2} \end{aligned}

and S^{−} ends in Γ; D ⊢_{P} Not_{G}(G_{1} ∧ G_{2})

Γ; D ⊢_{P} G_{1}  By subderivation
Γ; D ⊢_{P} G_{2}  By subderivation
Γ; D ⊢_{P} Not_{G}(G_{1}) ∨ Not_{G}(G_{2})  By rule Not_{G}∧
Subcase Γ; D ⊢_{P} Not_{G}(G_{1})  By inversion
⊥  By IH 1
Subcase Γ; D ⊢_{P} Not_{G}(G_{2})  By inversion
⊥  By IH 1

Case

S^{+} = \begin{aligned}Γ; D ⊢_{P} G_{1} \\ & ⊢ ∨ \\ Γ; D ⊢_{P} G_{1} ∨ G_{2} \end{aligned}

and S^{−} ends in Γ; D ⊢_{P} Not_{G}(G_{1} ∨ G_{2})

Draft of February 28, 2000

Γ; D ⊢_{P} G_{1}  By subderivation
Γ; D ⊢_{P} Not_{G}(G_{1}) ∧ Not_{G}(G_{2})  By rule Not_{G}∨
Γ; D ⊢_{P} Not_{G}(G_{1})  By inversion
Γ; D ⊢_{P} Not_{G}(G_{2})  By inversion
⊥  By IH 1

Case

S^{+} = \begin{aligned}Γ; D ⊢_{P} G_{2} \\ & ⊢ ∨ \\ Γ; D ⊢_{P} G_{1} ∨ G_{2} \end{aligned}

and S^{−} ends in Γ; D ⊢_{P} Not_{G}(G_{1} ∨ G_{2}). Symmetrical.

Case

S^{+} = \begin{aligned}(Γ, y:A); D ⊢_{P} [y/x]G′ \\ & ⊢∀^{∗} \\ Γ; D ⊢_{P} ∀x:a. DG′ \end{aligned}

and S^{−} ends in Γ; D ⊢_{P} Not_{G}(∀x:a. DG′):

(Γ, y:A); D ⊢_{P} [y/x]G′  By subderivation
Γ; D ⊢_{P} ∀x:a. DNot_{G}(G′)  By rule Not_{G}∀
(Γ, y:A); D ⊢_{P} [y/x]Not_{G}(G′)  By inversion
⊥  By IH 1

Case

S^{+} = \begin{aligned}Γ; (D ∧ D′) ⊢_{P} G′ \\ & ⊢ → \\ Γ; D ⊢_{P} D′ → G′ \end{aligned}

and S^{−} ends in Γ; D ⊢_{P} Not_{G}(D′ → G′):

Γ; (D ∧ D′) ⊢_{P} G′  By subderivation
Γ; D ⊢_{P} D′ → Not_{G}(G′)  By rule Not_{G} →
Γ; (D ∧ D′) ⊢_{P} Not_{G}(G′)  By inversion
⊥  By IH 1

Case The (dis)equality case follows from the decidability of the (dis)equality judgment.

□

Note that the proof goes through as there is no ‘bad’ interaction between the static and dynamic definition of a predicate; namely in subcase 2.2 there is no overlap between a clause from def(q, P) and def(¬q, D) since in every atomic assumption there must be an occurrence of a new parameter and every term at the same position in a program clause head must start with a constructor . Symmetrically for 2.3. Subcase 2.4 holds because an appropriate disequation is inferred; this approximates what happens in the first case 2.1, which is based on term exclusivity (Corollary ??). In the latter case, it suffices to consider, for D ∈ def(q, P), only Γ; D ⊢_{P} D>>Q and Γ; D ⊢_{P} Not_{D}(D)>>¬Q, because the positive definition is a conjunction, while the negative one is a disjunction; the same remark applies when the definition is dynamic (2.4).

The requirement for programs to only allow clause heads with rigid terms may seem too restrictive and we thus comment on it. As we remarked earlier, it applies only to non-Horn predicate definitions; secondly, if q \overline{M_{n}} ← G ⟹^{G} S is a hhf formula and say q N_{e_{x}}^{i} is in S for some 1 ≤ i ≤ n, then only M_{i} must be rigid. However, any program which uses a ‘catch-all‘ clause is forbidden; nevertheless it is easy to avoid catch-all clauses via coercion. Finally, we remark that any other (decidable) condition which avoids overlap between static and dynamic clauses will do; the one we have proposed is certainly not ‘ad hoc’ and is dictated by the practice of logical frameworks.

1.11 Exhaustivity

Theorem 1.28 (Exhaustivity) Let aug_{D}(P) ⟹^{D} S^{a} and Γ; D < S^{a}. If Γ; D ⊬_{P} G then Γ; D ⊢_{P} Not_{G}(G).

Proof: We generalize this to: let θ, σ be well-typed substitutions such that Γ ⊢ σ, Γ ⊢ θ:

1. If for all θ S^{−} :: Γ; [θ]D ⊬_{P} [θ]G, then there is a [σ] such that S^{+} :: Γ; [σ]D ⊢_{P} [σ]Not_{G}(G).

2.1 If, for all [θ] and D ∈ def(Q, P) I^{−} :: Γ; [θ]D ⊬_{P} [θ]D>>[θ]Q, then here is a [σ] such that I^{+} :: Γ; [σ]D ⊢_{P} [σ]Not_{D}(D)>>[σ]¬Q.

2.2 If, for all [θ] and D ∈ def(Q, D) I^{−} :: Γ; [θ]D ⊬_{P} [θ]D>>[θ]Q, then here is a [σ] such that I^{+} :: Γ; [σ]D ⊢_{P} [σ]Notα(D)>>[σ]¬Q.

The proof is by mutual induction on the structure of S^{−} and I^{−}.

2.1

Case

I^{−} = \frac{≯>⊤}{for all θ Γ; [θ]D ⊬_{P} ⊤>>[θ]Q}

as, for all θ [θ]⊤ = ⊤. Then Not_{D}(⊤) =⊥= [σ] ⊥ and

I^{+} = \frac{>> ⊥}{Γ; [θ]D ⊢_{P}⊥ >>[σ]¬Q}

Case

I^{−} = for all θ Γ; [θ]D ⊬_{P} [θ]\overline{N_{n}} =^{·} [θ]\overline{M_{n}} ≯> →^{1} for all θ Γ; [θ]D ⊬_{P} [θ](q \overline{N_{n}} ← G)>>[θ]q \overline{M_{n}}

Draft of February 28, 2000

for all θ Γ; [θ]D ⊬_{P} [θ]\overline{N_{n}} =^{·} [θ]\overline{M_{n}}  By subderivation
\overline{N_{n}} ≠ \overline{M_{n}}  By rule ⊬=^{·}
· ⊢ \overline{M_{n}} ∉ ∥\overline{N_{n}}∥  By definition of ∥ ∥
· ⊢ \overline{M_{n}} ∈ ∥Not(\overline{N_{n}})∥  By term exhaustivity (??)
\overline{M_{n}} = [ρ]\overline{S_{n}} for some ρ and \overline{S_{n}} ∈ Not(\overline{N_{n}})  By definition of ∥ ∥
Γ; [σ]D ⊢_{P} [σ]\overline{M_{n}} =^{·} [ρ · σ]\overline{S_{n}} some σBy rule and composition of subst.
Γ; [σ]D ⊢_{P} [σ](∀(q \overline{S_{n}} ← ⊤))>>[σ]¬q \overline{M_{n}}  By rule >>∀σ
Γ; [σ]D ⊢_{P} [σ](⋀_{\overline{S_{n}}∈Not(\overline{N_{n}})} ∀(q \overline{S_{n}} ← ⊤))>>[σ]¬q \overline{M_{n}} By rule >>∧

Γ; [σ]D ⊢_{P} [σ](⋀_{\overline{S_{n}}∈Not(\overline{N_{n}})} ∀(q \overline{S_{n}} ← ⊤) ∧ ¬q \overline{M_{n}} ← Not_{G}(G))>>[σ]¬q \overline{M_{n}}

By rule >>∧

Γ; [σ]D ⊢_{P} [σ]Not_{D}(q \overline{N_{n}} ← G)>>[σ]¬q \overline{M_{n}}  By rule Not_{D}>>

Case

I^{−} = for all θ Γ; [θ]D ⊬_{P} [θ]\overline{N_{n}} ≠^{·} [θ]\overline{M_{n}} for all θ Γ; [θ]D ⊬_{P} [θ]G ≯>→_{2} for all θ Γ; [θ]D ⊬_{P} [θ](q \overline{N_{n}} ← G)>>[θ]q \overline{M_{n}}

for all θ Γ; [θ]D ⊬_{P} [θ]\overline{N_{n}} ≠^{·} [θ]\overline{M_{n}}  By subderivation
Γ; [σ]D ⊢_{P} [σ]\overline{N_{n}} =^{·} [σ]\overline{M_{n}}  By rule ⊢≠^{·}
for all θ Γ; [θ]D ⊬_{P} [θ]G  By subderivation
Γ; [σ]D ⊢_{P} [σ]Not_{G}(G)  By IH 1
Γ; [σ]D ⊢_{P} [σ](¬q \overline{N_{n}} ← Not_{G}(G))>>[σ]¬q \overline{M_{n}}  By rule >> →

Γ; [σ]D ⊢_{P} [σ](∀(⋀_{\overline{S_{n}}∈Not(\overline{N_{n}})} q \overline{S_{n}} ← ⊤) ∧ ¬q \overline{N_{n}} ← Not_{G}(G))>>[σ]¬q \overline{M_{n}}

By rule >>∧

Γ; [σ]D ⊢_{P} [σ]Not_{D}(q \overline{N_{n}} ← G)>>[σ]¬q \overline{M_{n}}  By rule Not_{D} →

Case

I^{−} = for all θ Γ; [θ]D ⊬_{P} [θ]D_{1}>>[θ]Q ≯>∨_{1} for all θ Γ; [θ]D ⊬_{P} [θ](D_{1} ∨ D_{2})>>[θ]q
for all θ Γ; [θ]D ⊬_{P} [θ]D_{1}>>[θ]Q  By subderivation
Γ; [σ]D ⊢_{P} [σ]Not_{D}(D_{1})>>[σ]¬Q  By IH 2.1
Γ; [σ]D ⊢_{P} [σ]Not_{D}(D_{1}) ∧ [σ]Not_{D}(D_{2})>>[σ]¬Q  By rule >>∧_{1}
Γ; [σ]D ⊢_{P} [σ]Not_{D}(D_{1} ∨ D_{2})>>[σ]¬Q  By rule Not_{D}∨

Case

I^{−} = for all θ Γ; [θ]D ⊬_{P} [θ]D_{2}>>[θ]Q ≯>∨_{2} for all θ Γ; [θ]D ⊬_{P} [θ](D_{1} ∨ D_{2})>>[θ]q

Symmetrical to the above Case

I^{−} = for all θ Γ; [θ]D ⊬_{P} [θ]D_{1}>>[θ]Q for all θ Γ; [θ]D ⊬_{P} [θ]D_{2}>>[θ]Q ≯>∧ for all θ Γ; [θ]D ⊬_{P} [θ](D_{1} ∧ D_{2})>>[θ]Q

for all θ Γ; [θ]D ⊬_{P} [θ]D_{1}>>[θ]Q  By subderivation
for all θ Γ; [θ]D ⊬_{P} [θ]D_{2}>>[θ]Q  By subderivation

Γ; [σ]D ⊢_{P} [σ]Not_{D}(D_{1})>>[σ]¬Q  By IH 2.1
Γ; [σ]D ⊢_{P} [σ]Not_{D}(D_{2})>>[σ]¬Q  By IH 2.1
Γ; [σ]D ⊢_{P} [σ]Not_{D}(D_{1}) ∨ [σ]Not_{D}(D_{2})>>[σ]¬Q  By rule >>∨
Γ; [σ]D ⊢_{P} [σ]Not_{D}(D_{1} ∧ D_{2})>>[σ]¬Q  By rule Not∧

Case

I^{−} = for all θ, n, Γ; [θ]D ⊬_{P} [θ, n/x]D>>[θ]Q ≯>∀ for all θ Γ; [θ]D ⊬_{P} [θ]∀x:A. D>>[θ]Q
for all [θ], n, Γ; [θ]D ⊬_{P} [θ] · [n/x]D>>[θ]Q  By subderivation
Γ; [σ]D ⊢_{P} [σ] · [t/x]Not_{D}(D)>>[σ]¬Q  By IH 2.1
Γ; [σ]D ⊢_{P} [σ]∀x:A. Not_{D}(D)>>[σ]¬Q  By rule >>∀
Γ; [σ]D ⊢_{P} [σ]Not_{D}(∀x:A. D)>>[σ]¬Q  By rule Not_{D}∀

2.2 Case

I^{−} = \frac{≯>⊤}{for all θ Γ; D ⊬_{P} ⊤_{q}>>[θ]q \overline{M_{e_{x}}^{i}}}

\overline{M_{e_{x}}^{i}} = \overline{M_{e_{x}}^{i}}  By hypothesis
Γ; D ⊢_{P} [σ] · [\overline{M_{e_{x}}^{i}}/\overline{Z_{n}}]Z_{ex}^{i} =^{·} [σ]\overline{M_{e_{x}}^{i}}  By rule ⊢=^{·}
Γ; D ⊢_{P} [σ]∀Z_{1} :A_{1}…. ∀Z_{n}:A_{n}. ¬q \overline{Z_{e_{x}}^{i}}>>[σ]¬q \overline{M_{e_{x}}^{i}}By rule >>∀
Γ; D ⊢_{P} [σ]Not_{x}^{i}(⊤_{q})>>[σ]¬q \overline{M_{e_{x}}^{i}}  By rule Not_{x}^{i}⊤
Γ; D ⊢_{P} [σ] ⋀_{x∈dom(Γ)} ⋀_{xR^{i}q} Not_{x}^{i}(⊤_{q})>>[σ]¬q \overline{M_{e_{x}}^{i}} By rule >>∧
Γ; D ⊢_{P} [σ]Notα(⊤_{q})>>[σ]¬q \overline{M_{e_{x}}^{i}}  By rule Notα⊤

Case

I^{−} = for all θ Γ; [θ]D ⊬_{P} [θ]\overline{N_{e_{x}}^{i}} =^{·} [θ]\overline{M_{e_{x}}^{i}} ≯> →^{1} for all θ Γ; [θ]D ⊬_{P} [θ](q \overline{N_{e_{x}}^{i}} ← G)>>[θ]q \overline{M_{e_{x}}^{i}}

for all θ Γ; [θ]D ⊬_{P} [θ]\overline{N_{e_{x}}^{i}} =^{·} q \overline{M_{e_{x}}^{i}}  By subderivation
for all θ Γ; [θ]D ⊬_{P} [θ]N_{j} =^{·} [θ]M_{j} for some 1 ≤ j ≤ n, j ≠ iBy rule ⊬=^{·}
Γ; [σ]D ⊢_{P} [σ]N_{j} ≠^{·} [σ]M_{j}  By rule ⊢≠^{·}
Γ; [σ]D ⊢_{P} [σ] · [\overline{M_{e_{x}}^{i}}/\overline{Z_{n}}](¬q Z_{e_{x}}^{i} ← N_{j} ≠^{·} Z_{j})>>[σ]¬q \overline{M_{e_{x}}^{i}}By rule >> →

Γ; [σ]D ⊢_{P} [σ](∀Z_{1} :A_{1}…. ∀Z_{n}:A_{n}. ¬q Z_{e_{x}}^{i} ← N_{j} ≠^{·} Z_{j})>>[σ]¬q \overline{M_{e_{x}}^{i}}

By rule >>∀

Γ; [σ]D ⊢_{P} [σ]Not_{x}^{i}(q \overline{N_{e_{x}}^{i}} ← ⊤)>>[σ]¬q \overline{M_{e_{x}}^{i}} some 1 ≤ i ≤ n, i ≠ j

By rule Not_{x}^{i}At

Γ; [σ]D ⊢_{P} [σ]Not_{x}^{i}(q \overline{N_{e_{x}}^{i}})>>[σ]¬q \overline{M_{e_{x}}^{i}}  By rule >>∧

Γ; [σ]D ⊢_{P} [σ] ⋀_{x∈dom(Γ)} ⋀_{xR^{i}q} Not_{x}^{i}(q \overline{N_{e_{x}}^{i}}) ∧ ¬(q \overline{N_{e_{x}}^{i}} ← G)>>[σ]¬q \overline{M_{e_{x}}^{i}}

By rule >>∧

Γ; [σ]D ⊢_{P} [σ]Notα(q \overline{N_{e_{x}}^{i}} ← G)>>[σ]¬q \overline{M_{e_{x}}^{i}} By rule Notα →

Case

I^{−} = for all θ Γ; [θ]D ⊬_{P} [θ]\overline{N_{e_{x}}^{i}} ≠^{·} [θ]\overline{M_{e_{x}}^{i}} for all θ Γ; [θ]D ⊬_{P} [θ]G ≯>→_{2} for all θ Γ; [θ]D ⊬_{P} [θ](q \overline{N_{e_{x}}^{i}} ← G)>>[θ]q \overline{M_{e_{x}}^{i}}

for all θ Γ; [θ]D ⊬_{P} [θ]\overline{N_{e_{x}}^{i}} ≠^{·} [θ]\overline{M_{e_{x}}^{i}}  By subderivation
Γ; [σ]D ⊢_{P} [σ]\overline{N_{e_{x}}^{i}} =^{·} [σ]\overline{M_{e_{x}}^{i}}  By rule ⊢≠^{·}
for all θ Γ; [θ]D ⊬_{P} [θ]G  By subderivation
Γ; [σ]D ⊢_{P} [σ]Not_{G}(G)  By IH 1
Γ; [σ]D ⊢_{P} [σ](¬q \overline{N_{e_{x}}^{i}} ← Not_{G}(G))>>[σ]¬q \overline{M_{e_{x}}^{i}} By rule >> →

Γ; [σ]D ⊢_{P} [σ] ⋀_{x∈dom(Γ)} ⋀_{xR^{i}q} Not_{x}^{i}(q \overline{M_{e_{x}}^{i}}) ∧ ¬q \overline{M_{e_{x}}^{i}} ← Not_{G}(G))>>[σ]¬q \overline{M_{e_{x}}^{i}}

By rule >>∧

Γ; [σ]D ⊢_{P} [σ]Notα(q \overline{N_{e_{x}}^{i}} ← G)>>[σ]¬q \overline{M_{e_{x}}^{i}} By rule Notα →

Case

I^{−} = for all θ Γ; [θ]D ⊬_{P} [θ]D_{1}>>[θ]Q ≯>∨_{1} for all θ Γ; [θ]D ⊬_{P} [θ](D_{1} ∨ D_{2})>>[θ]q
for all θ Γ; [θ]D ⊬_{P} [θ]D_{1}>>[θ]Q  By subderivation
Γ; [σ]D ⊢_{P} [σ]Notα(D_{1})>>[σ]¬Q  By IH 2.2
Γ; [σ]D ⊢_{P} [σ]Notα(D_{1}) ∧ [σ]Notα(D_{2})>>[σ]¬Q By rule >>∧_{1}
Γ; [σ]D ⊢_{P} [σ]Notα(D_{1} ∨ D_{2})>>[σ]¬Q  By rule Notα∨

Case

I^{−} = for all θ Γ; [θ]D ⊬_{P} [θ]D_{2}>>[θ]Q ≯>∨_{2} for all θ Γ; [θ]D ⊬_{P} [θ](D_{1} ∨ D_{2})>>[θ]q

Symmetrical to the above Case

I^{−} = for all θ Γ; [θ]D ⊬_{P} [θ]D_{1}>>[θ]Q for all θ Γ; [θ]D ⊬_{P} [θ]D_{2}>>[θ]Q ≯>∧ for all θ Γ; [θ]D ⊬_{P} [θ](D_{1} ∧ D_{2})>>[θ]Q

for all θ Γ; [θ]D ⊬_{P} [θ]D_{1}>>[θ]Q  By subderivation
for all θ Γ; [θ]D ⊬_{P} [θ]D_{2}>>[θ]Q  By subderivation
Γ; [σ]D ⊢_{P} [σ]Notα(D_{1})>>[σ]¬Q  By IH 2.2
Γ; [σ]D ⊢_{P} [σ]Notα(D_{2})>>[σ]¬Q  By IH 2.2
Γ; [σ]D ⊢_{P} [σ]Notα(D_{1}) ∨ [σ]Notα(D_{2})>>[σ]¬Q By rule >>∨
Γ; [σ]D ⊢_{P} [σ]Notα(D_{1} ∧ D_{2})>>[σ]¬Q  By rule Not∧

Case

I^{−} = for all [θ], n, Γ; [θ]D ⊬_{P} [θ] · [n/x]D>>[θ]Q ≯>∀ for all θ Γ; [θ]D ⊬_{P} [θ]∀x:A. D>>[θ]Q
for all [θ], n, Γ; [θ]D ⊬_{P} [θ] · [n/x]D>>[θ]Q  By subderivation
Γ; [σ]D ⊢_{P} [σ] · [t/x]Notα(D)>>[σ]¬Q  By IH 2.2
Γ; [σ]D ⊢_{P} [σ]∀x:A. Notα(D)>>[σ]¬Q  By rule >>∀
Γ; [σ]D ⊢_{P} [σ]Notα(∀x:A. D)>>[σ]¬Q  By rule Notα∀

Case

S^{−} = for all θ Γ; [θ]D ⊬_{P} [θ]def(Q, P ∧ D)>>[θ]Q ⊬ atm for all θ Γ; [θ]D ⊬_{P} [θ]Q

Subcase D ∈ def(Q, P)

for all θ Γ; [θ]D ⊬_{P} [θ]D>>[θ]Q  By subderivation
Γ; [σ]D ⊢_{P} [σ]Not_{D}(D)>>[σ]¬Q  By IH 2.1
Γ; [σ]D ⊢_{P} [σ]def(¬Q, P)>>¬Q  By rule >>∨
Γ; [σ]D ⊢_{P} [σ]Not_{G}(Q)  By rule ⊢ At

Subcase D ∈ def(Q, D)

for all θ Γ; [θ]D ⊬_{P} [θ]D>>[θ]Q  By subderivation
Γ; [σ]D ⊢_{P} [σ]Notα(D)>>[σ]¬Q  By IH 2.2
Γ; [σ]D ⊢_{P} [σ]def(¬Q, D)>>¬Q  By rule >>∨
Γ; [σ]D ⊢_{P} [σ](Q)  By rule ⊢ At

Case

S^{−} = \frac{⊬ ⊥}{Γ; [θ]D ⊬_{P} ⊥}

Then Not_{G}(⊥) = [σ]⊤ = ⊤ and

S^{+} = \frac{⊢ ⊤}{Γ; [σ]D ⊢_{P} [σ]Not_{G}(⊤)}

Case

S^{−} = for all θ Γ; [θ]D ⊬_{P} [θ]G_{1} for all θ Γ; [θ]D ⊬_{P} [θ]G_{2} ⊬ ∨ for all θ Γ; [θ]D ⊬_{P} [θ](G_{1} ∨ G_{2})

for all θ Γ; [θ]D ⊬_{P} [θ]G_{1}  By subderivation
for all θ Γ; [θ]D ⊬_{P} [θ]G_{2}  By subderivation
Γ; [σ]D ⊢_{P} [σ]Not_{G}(G_{1})  By IH 1
Γ; [σ]D ⊢_{P} [σ]Not_{G}(G_{2})  By IH 1
Γ; [σ]D ⊢_{P} [σ]Not_{G}(G_{1}) ∧ [σ]Not_{G}(G_{2})  By rule ⊢ ∧
Γ; [σ]D ⊢_{P} [σ]Not_{G}(G_{1} ∨ G_{2})  By rule Not_{G}∧

Case

S^{−} = for all θ Γ; [θ]D ⊬_{P} [θ]G_{1} ⊬ ∧_{1} for all θ Γ; [θ]D ⊬_{P} [θ](G_{1} ∧ G_{2})
for all θ Γ; [θ]D ⊬_{P} [θ]G_{1}  By subderivation
Γ; [σ]D ⊢_{P} [σ]Not_{G}(G_{1})  By IH 1
Γ; [σ]D ⊢_{P} [σ]Not_{G}(G_{1}) ∨ [σ]Not_{G}(G_{2})  By rule ⊢ ∨
Γ; [σ]D ⊢_{P} [σ]Not_{G}(G_{1} ∧ G_{2})  By rule Not_{G}∨

Case

S^{−} = for all θ Γ; [θ]D ⊬_{P} [θ]G_{2} ⊬ ∧_{2} for all θ Γ; [θ]D ⊬_{P} [θ](G_{1} ∧ G_{2})

Symmetrical to the above. Case

S^{−} = for all θ Γ; [θ]D ∧ [θ]D ⊬_{P} [θ]G′ ⊬ → for all θ Γ; [θ]D ⊬_{P} [θ](D′ → G′)

Draft of February 28, 2000

for all θ Γ; [θ]D ∧ [θ]D′ ⊬_{P} [θ]G′  By subderivation
Γ; [σ]D ∧ [σ]D ⊢_{P} [σ]Not_{G}(G′)  By IH 1
Γ; [σ]D ⊢_{P} [σ]D′ → [σ]Not_{G}(G′)  By rule ⊢→
Γ; [σ]D ⊢_{P} [σ](D′ → Not_{G}(G′))  By rule Not_{G} →
Γ; [σ]D ⊢_{P} [σ]Not_{G}(D′ → G′)  By subst.

Case

S^{−} = for all θ (Γ, y:A); [θ]D ⊬_{P} [θ] · [y/x]G ⊬∀ Γ; [θ]D ⊬_{P} [θ]∀x:a. DG′
for all θ (Γ, y:A); [θ]D ⊬_{P} [θ] · [y/x]G  By subderivation
(Γ, y:A); [σ]D ⊢_{P} [σ] · [y/x]Not_{G}(G′)  By IH 1
(Γ, y:A); [σ]D ⊢_{P} [σ]∀x:A. Not_{G}(G′)  By rule ⊢ ∀
Γ; [σ]D ⊢_{P} [σ]Not_{G}(∀x:a. DG′)  By rule Not_{G}∀

Case (dis)equations: immediate.

□

1.12 Refinements

In the following Subsections we will move towards an operational semantics for our language.

1.12.1 Elimination of ∨

We now show how to eliminate the ∨ operator preserving provability; this will recover uniformity in proof-search. We generalize the approach in [BMPT90], where the operation was defined as follows: for m1 : Q_{1} ← G_{1} and m2 : Q_{2} ← G_{2}:

m1 ∨ m2 = θ(Q_{1} ← G_{1} ∧ G_{2}) where θ = mgu(Q_{1}, Q_{2})

As we remarked earlier, the ∨ operator was introduced to preserve the duality between conjunction and disjunction in clauses. Its use is limited to clauses in the same predicate definition and therefore it can be eliminated simulating unification in the definition. Yet, the strict higher-order unification problem is quite complex and even more so complicated by the mixed quantifier structure of hhf. Moreover, we have already in our language parameter (dis)equations introduced by the augmentation procedure, as well as variable-variable (dis)equations stemming from left-linearization. We thus choose to compile our source into an intermediate language which makes unification problems explicit as simple equational problems in the style of the unification logic introduced in [Pfe91]. We can then perform constraint simplification as used in Elf [Pfe89] and Twelf [SP98].

We adapt the residuation technique used in [Pfe92] to compile immediate implication into resolution. We define the judgment D_{1} ∨ D_{2} \ D in Figure 1.12.1 by induction on (normalized) D_{1}, with the intended meaning of ‘D_{1} ∨ D_{2} compiles to D’: As usual, we add the rules symmetric to ∨⊤, ∨∀, ∨∧. Note that

\frac{∨⊤}{⊤ ∨ D \ ⊤}

\frac{∨atm}{(q N⃗_{1} ← G_{1}) ∨ (q N⃗_{2} ← G_{2}) \ q N⃗_{1} ← (N⃗_{1} =^{·} N⃗_{2}) ∧ G_{1} ∧ G_{2}}

([u/x]D_{1}) ∨ D_{2} \ [u/x]D

∨∀ (∀x:A. D_{1}) ∨ D_{2} \ ∀x:A. D

D_{1} ∨ D_{2} \ D D′_{1} ∨ D_{2} \ D′

∨∧

(D_{1} ∧ D′_{1}) ∨ D_{2} \ D ∧ D′

Figure 1.13: ∨-Elimination. Judgment D_{1} ∨ D_{2} \ D

residuation is undefined for clauses with different heads; yet we could make the judgment total by agreeing to compile them to ⊤.

Example 1.29 Continuing Example 1.20; recall that

Not_{D}(cloz) =
∀F:exp. ¬closed (lam F) ∧ ∀F_{1}, F_{2} :exp. ¬closed (app F_{1} F_{2}).
Not_{D}(clolam) =
¬closed z ∧ ∀F_{1}, F_{2} :exp. ¬closed (app F_{1} F_{2}) ∧
∀E:exp. ¬closed (lam E) ← ∀x:exp. (closed x → ¬closed (E x)).

Let us compute Not_{D}(cloz) ⊗ Not_{D}(clolam) \ D:

∀F:exp. ¬closed (lam F) ← (lam F) =^{·} z ∧

∀F, F_{1}, F_{2} :exp. ¬closed (lam F) ← (lam F) =^{·} (app F_{1} F_{2}) ∧

∀E:exp. ¬closed (lam E) ← (∀x:exp. closed x → ¬closed (E x)) ∧

∀F_{1}, F_{2} :exp. ¬closed (app F_{1} F_{2}) ← (app F_{1} F_{2}) =^{·} z ∧

∀F, F_{1}, F_{2} :exp. ¬closed (app F_{1} F_{2}) ← (app F_{1} F_{2}) =^{·} (lam F) ∧

∀F_{1}, F_{2} :exp. ¬closed (app F_{1} F_{2}).

Note that only the third and last clause are satisfiable.

The following lemma guarantees that compilation preserves immediate entailment:

Lemma 1.30 Let D_{1} ∨ D_{2} \ D: then Γ; D ⊢ D_{1} ∨ D_{2}>>Q iff Γ; D ⊢ D>>Q.

Proof: (→). By induction on the structure of π :: D_{1} ∨ D_{2} \ D.

Case π ends in \⊤. Trivially true.

Case

π = \frac{∨atm}{(q N⃗_{1} ← G_{1}) ∨ (q N⃗_{2} ← G_{2}) \ q N⃗_{1} ← (N⃗_{1} =^{·} N⃗_{2}) ∧ G_{1} ∧ G_{2}}

Γ; D ⊢_{P} (q N⃗_{1} ← G_{1}) ∨ (q N⃗_{2} ← G_{2})>>q N⃗  By hypothesis
Γ; D ⊢_{P} q N⃗_{1} ← G_{1}>>q N⃗ and q N⃗_{2} ← G_{2}>>q N⃗  By inversion
Γ; D ⊢_{P} N⃗_{1} =^{·} N⃗ and Γ; D ⊢_{P} G_{1}  By inversion
Γ; D ⊢_{P} N⃗_{2} =^{·} N⃗ and Γ; D ⊢_{P} G_{2}  By inversion
Γ; D ⊢_{P} N⃗_{1} =^{·} N⃗_{2}  By replacement
Γ; D ⊢_{P} q N⃗_{1} ← (N⃗_{1} =^{·} N⃗_{2}) ∧ G_{1} ∧ G_{2}>>q N⃗  By rule (s)

Case π ends in ∨∧, ∨∀: by an immediate appeal to the IH. (←): completely analogous. □ We remark that, using again terminnating programs, the above Lemma covers immediate denial as well.

We now extend the effect of the above compilation on a program: Definition 1.31

⊤^{∨_{D}} = ⊤
⊥^{∨_{D}} = ⊥
Q ← G^{∨_{D}} = Q ← G^{∨_{G}}
D_{1} ∧ D_{2}^{∨_{D}} = D_{1}^{∨_{D}} ∧ D_{2}^{∨_{D}}
∀x:A. D^{∨_{D}} = ∀x:A. D^{∨_{D}}
D_{1} ∨ D_{2}^{∨_{D}} = D  where D_{1}^{∨_{D}} ∨ D_{2}^{∨_{D}} \ D
X^{∨_{G}} = X  X ∈ {⊤, ⊥, Q, (dis)eq}
G_{1} ∧ G_{2}^{∨_{G}} = G_{1}^{∨_{G}} ∧ G_{2}^{∨_{G}}
G_{1} ∨ G_{2}^{∨_{G}} = G_{1}^{∨_{G}} ∨ G_{2}^{∨_{G}}
D → G^{∨_{G}} = D^{∨_{D}} → G^{∨_{G}}
∀x:A. G^{∨_{G}} = ∀x:A. G^{∨_{G}}
∃x:A. G^{∨_{G}} = ∃x:A. G^{∨_{G}}

Theorem 1.32 (Elimination of ∨)

1. S :: Γ; D ⊢_{P} G iff ∨S :: Γ; D^{∨_{D}} ⊢_{P} G^{∨_{G}};

2. I :: Γ; D ⊢_{P} D>>Q iff ∨I :: Γ; D^{∨_{D}} ⊢_{P} D^{∨_{D}}>>Q. Proof: (→). By a straightforward mutual induction on the structure of the given derivations: we show the crucial case. Case I ends in >>∨:

Γ; D ⊢_{P} D_{1}>>Q and Γ; D ⊢_{P} D_{2}>>Q  By subderivation
Γ; D^{∨_{D}} ⊢_{P} D_{1}^{∨_{D}}>>Q and Γ; D^{∨_{D}} ⊢_{P} D_{2}^{∨_{D}}>>Q  By IH 2
Γ; D^{∨_{D}} ⊢_{P} D_{1}^{∨_{D}} ∨ D_{2}^{∨_{D}}>>Q  By rule >>∨
Γ; D^{∨_{D}} ⊢_{P} D_{1} ∨ D_{2}^{∨_{D}}>>Q  By Lemma 1.30

(←). Similarly. □ The same remark w.r.t. termination applies.

1.12.2 Constraint Simplification

In this section we hint on how to bring clauses stemming from complementation into their final format by simplifying, whenever possible, the disequation introduced by the Notα → rule. This entails the following:

• Solving existential variable-ground term disequations by computing the complement of the latter.

• Removing unsatisfiable variable-variable disequations.

In a final pass we may also:

• Remove irrelevant occurrences of ⊤.

• Hide the irrelevant augmentation in the final negative clause.

• If so desired and when possible, bring clauses to the ‘core’ languages syntax, as in LF.

Example 1.33 Continuing Example 1.20 and 1.29 the final definition of ¬closed is:

oplam : ∀E:exp. open (lam E) ← ∀x:exp. open (E x).
opap1 : ∀E_{1}, E_{2} :exp. open (app E_{1} E_{2}) ← open E_{1}.
opap2 : ∀E_{1}, E_{2} :exp. open (app E_{1} E_{2}) ← open E_{2}.

where we have solved all disequations, which are in this case trivial groundground checks, hidden the irrelevant assumption closed x and renamed ‘¬closed’ into open.

Example 1.34 The final definition of ¬linear and in turn ¬linx is:

¬linapp1 : ¬linear(app E_{1} E_{2}) ← ¬linear(E_{1}).
¬linapp2 : ¬linear(app E_{1} E_{2}) ← ¬linear(E_{2}).
¬linlam1 : ¬linear(lam λx . E x) ← ¬linx(lam λx . E x)
.¬linlam2 : ¬linear(lam λx . E x) ← ∀x:exp. linear(E x).
¬linx1 : ¬linx(λx . app (E_{1} x) (E_{2} x)) ← strict(E_{2} x).
¬linx2 : ¬linx(λx . app (E_{1} x) (E_{2} x)) ← strict(E_{1} x).
¬linxap1 : ¬linx(λx . app (E_{1} x) E_{2}) ← ¬linx(λx . E_{1} x).
¬linxap2 : ¬linx(λx . app E_{1} (E_{2} x)) ← ¬linx(λx . E_{2} x).
¬linxlm : ¬linx(λx . lam(λy . E x y)) ←

(∀y:exp. ¬linx(λx . y) → ¬linx(λx . E x y)).

Bibliography

[Acz77] Peter Aczel. An introduction to inductive definitions. In J. Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, chapter C.7, pages 739– 782. North-Holland, Amsterdam, 1977.

[Apt90] Krzysztof R. Apt. Logic programming. In J. van Leewen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 10, pages 493–574. The MIT Press, New York, N.Y., 1990.

[BM90] Anthony J. Bonner and L. Thorne McCarty. Adding negation-as-failure to intuitionistic logic programming. In Saumya Hermenegildo Manuel Debray, editor, Proceedings of the 1990 North American Conference on Logic Programming, pages 671–693, Austin, TX, October 1990. MIT Press.

[BMPT90] Roberto Barbuti, Paolo Mancarella, Dino Pedreschi, and Franco Turini. A transformational approach to negation in logic programming. Journal of Logic Programming, 8:201–228, 1990.

[BMV89] A. J. Bonner, L. T. McCarty, and K. Vadaparty. Expressing Database Queries with Intuitionistic Logic. In Ewing L. Lusk and Ross A. Overbeek, editors, Proceedings of the North American Conference on Logic Programming, pages 831–850, Cleveland, Ohio, USA, 1989.

[Bon91] A.J. Bonner. Hypothetical Reasoning in Deductive Databases. PhD thesis, Rutgers University, October 1991.

[Bon94] A.J. Bonner. Hypothetical reasoning with intuitionistic logic. In R. Demolombe and T. Imielinski, editors, Non-Standard Queries and Answers, volume 306 of Studies in Logic and Computation, pages 187–219. Oxford University Press, 1994.

[Cla78] K. L. Clark. Negation as failure. In H. Gallaire and J. Minker, editors, Logic and Databases, pages 293–322. Plenum Press, New York, 1978.

[Dun92] P. M. Dung. Declarative semantics of hypothetical logic programming with negation as failure. In E. Lamma and P. Mello, editors, Proceedings of the Third International Workshop on Extensions of Logic Programming (ELP ’92), volume 660 of LNAI, pages 45–58, Bologna, Italy, February 1992. Springer Verlag.

[Eri93] Lars-Henrik Eriksson. Finitary Partial Inductive Definitions and General Logic. PhD thesis, Department of Computer and System Sciences, Royal Institute of Technology, Stockholm, 1993.

[Gab85] Dov M. Gabbay. N-Prolog: An extension of prolog with hypothetical implications II. logical foundations and negation as failure. Journal of Logic Programming, 2(4):251–283, December 1985.

[GL90] Michael Gelfond and Vladimir Lifschitz. Logic programs with classical negation. In David H.D. Szerdei Peter Warren, editor, Proceedings of the 7th International Conference on Logic Programming (ICLP ’90), pages 579–597, Jerusalem, June 1990. MIT Press.

[GMR92] L. Giordano, A. Martelli, and G. Rossi. Extending Horn clause logic with implication goals. Theoretical Computer Science, 95(1):43–74, March 1992.

[GO98] Laura Giordano and Nicola Olivetti. Negation as failure and embedded implication. Journal of Logic Programming, to appear, 1998.

[GR84] Dov M. Gabbay and U. Reyle. N-Prolog: An extension of prolog with hypothetical implications I. Journal of Logic Programming, 1(4):319–355, December 1984.

[Hal91] L. Hallnas. Partial inductive definitions. Theoretical Computer Science, 87(1):115–147, July 1991.

[Har89] J. Harland. A Kripke-like Model for Negation as Failure. In Ewing L. Lusk and Ross A. Overbeek, editors, Proceedings of the North American Conference on Logic Programming, pages 626–644, Cleveland, Ohio, USA, 1989.

[Har91] James Harland. On Hereditary Harrop Formulae as a Basis for Logic Programming. PhD thesis, Edinburgh, January 1991.

[Har93] James Harland. Success and failure for hereditary Harrop formulae. Journal of Logic Programming, 17(1):1–29, October 1993.

[HM94] Joshua Hodas and Dale Miller. Logic programming in a fragment of intuitionistic linear logic. Information and Computation, 110(2):327–365, 1994. A preliminary version appeared in the Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, pages 32–42, Amsterdam, The Netherlands, July 1991.

[HSH90] L. Hallnas and P. Schroeder-Heister. A proof-theoretic approach to logic programming: Clauses as rules. Journal of Logic and Computation, 1(2):635-660, October 1990.

[HSH91] L. Hallnas and P. Schroeder-Heister. A proof-theoretic approach to logic programming: Programs as definitions. Journal of Logic and Computation, 1(5):261-283, October 1991.

[KNW93] Keehand Kwon, Gopalan Nadathur, and Debra Sue Wilson. Implementing a notion of modules in the logic programming language λProlog. In E. Lamma and P. Mello, editors, Proceedings of the Third International Workshop on Extensions of Logic Programming, pages 359–393, Bologna, Italy, February 1993. Springer-Verlag LNAI 660.

[Kre92] Per Kreuger. GCLA II. a definitional approach to control. Technical Report R92:09, SICS, 1992.

[MAK91] L. Hallnass Martin Aronson, L-H. Eriksson and P. Kreuger. A survey of GCLA: a definitional approach to logic programming. In Peter Schroeder-Heister, editor, Proceedings of the First International Workshop on Extensions of Logic Programming, volume 1050 of 475, pages 19–34, Berlin, March28–30 1991. Springer.

[McC88a] L. Thorne McCarty. Clausal intuistionistic logic: I. fixed point semantics. Journal of Logic Programming, 5(1):1–31, March 1988.

[McC88b] L. Thorne McCarty. Clausal intuitionistic logic II. tableau proof procedure. Journal of Logic Programming, 5:93–132, 1988.

[Mil89] Dale Miller. A logical analysis of modules in logic programming. Journal of Logic Programming, 6(1-2):79–108, January 1989.

[MM97] Raymond McDowell and Dale Miller. A logic for reasoning with higher-order abstract syntax: An extended abstract. In Glynn Winskel, editor, Proceedings of the Twelfth Annual Symposium on Logic in Computer Science, pages 434–445, Warsaw, Poland, June 1997.

[MMP88] Paolo Mancarella, Simone Martini, and Dino Pedreschi. Complete logic Programs with domain-closure Axiom. Journal of Logic Programming, 5:263–276, 1988.

[Mom92] Alberto Momigliano. Minimal negation and hereditary Harrop formulae. In Anil Nerode and Mikhail Taitslin, editors, Proceedings of Logical Foundations of Computer Science (Tver ’92), volume 620 of LNCS, pages 326–335, Berlin, Germany, July 1992. Springer.

[Nel49] D. Nelson. Constructive falsity. Journal of Symbolic Logic, pages 16–26, 1949.

[NL92] Olivetti N. and Terracini L. N-Prolog and the equivalence of logic program. Journal of Logic Language and Information, 5:253-3392, 1992.

[NL95] Gopalan Nadathur and Donald W. Loveland. Uniform proofs and disjunctive logic programming. In D. Kozen, editor, Proceedings of the Tenth Annual Symposium on Logic in Computer Science, pages 148–155, San Diego, California, June 1995. IEEE Computer Society Press. Available as Technical Report CS-1994-40, Department of Computer Science, Duke University, December 1994.

[Pea90] David Pearce. Reasoning with negative information, II: Hard negation, strong negation and logic programs. In H. Pearce, D.; Wansing, editor, Proceedings of the International Workshop on Nonclassical Logics and Information Processing, volume 619 of LNAI, pages 63– 79, Berlin, FRG, November 1990. Springer Verlag.

[Pfe89] Frank Pfenning. Elf: A language for logic definition and verified meta-programming. In Fourth Annual Symposium on Logic in Computer Science, pages 313–322, Pacific Grove, California, June 1989. IEEE Computer Society Press.

[Pfe91] Frank Pfenning. Logic programming in the LF logical framework. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 149–181. Cambridge University Press, 1991.

[Pfe92] Frank Pfenning. Computation and deduction. Unpublished lecture notes, 277 pp. Revised May 1994, April 1996, May 1992.

[Rei78] R. Reiter. On closed world databases. In Gallaire and Minker, editors, Logic and Databases, pages 55–76. Plenum Press, New York, 1978.

[RP96] Ekkehard Rohwedder and Frank Pfenning. Mode and termination checking for higher-order logic programs. In Hanne Riis Nielson, editor, Proceedings of the European Symposium on Programming, pages 296–310, Linköping, Sweden, April 1996. Springer-Verlag LNCS 1058.

[SH93] Peter Schroeder-Heister. Rules of definitional reflection. In M. Vardi, editor, Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science, pages 222–232, Montreal, Canada, June 1993.

[SP98] Carsten Schürmann and Frank Pfenning. Automated theorem proving in a simple meta-logic for LF. In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction (CADE-15), pages 286–300, Lindau, Germany, July 1998. Springer-Verlag LNCS 1421.

[Vir99] Roberto Virga. Higher-Order Rewriting with Dependent Types. PhD thesis, Department of Mathematical Sciences, Carnegie Mellon University, 1999. Forthcoming.

[Wan93] Heinrich Wansing. The logic of information structures, volume 681 of Lecture Notes in Artificial Intelligence and Lecture Notes in Computer Science. Springer-Verlag Inc., New York, NY, USA, 1993. Revision of the author’s doctoral thesis (Fachbereich Philosophie und Sozialwissenschaften I of the Free University of Berlin).