1 Clause Complementation

Source language: Let M⃗, N⃗ be sequences of simple terms:

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

Note that ‘facts’ are represented, in a standardized way, by Q ← ⊤. Remark also that Not is not a connective, but a name constructor for atomic formulae.

We now introduce in Figure 1 and 1 the rules for (static) clause and goal complemetation. We collect essentially existential variables in a pool Φ left here, for the moment, implicit. Π(Q ← ⊤) denotes the universal closure of the free variables in Q. In Not_{G}Π the asterisk reminds of the eigenvariable condition on a.

Note that rule Not_{D} → is where all the work is done: a set of negative facts is built via Not(M⃗), whose fresh free variables are universally closed and the negative counterpart of the source clause is obtained via complementation of the body. The original quantification is retained thanks to rule Not_{D}Π.

\frac{Not_{D}⊤}{Not_{D}(⊤) =⊥}  \frac{Not_{D} ⊥}{Not_{D}(⊥) = ⊤}
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}
Not_{G}(G) = G′
Not ←

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

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

Definition 1.1 (def(q, D))

def(q, ⊤) = ⊤_{q}

\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}([a/x]G) = [a/x]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 2: Goal Complementation: Not_{G}(G) = G′

def(q, ⊥) = ⊥_{q}
def(q, q M⃗ ← G) = q ← G
def(q, q′ M⃗ ← G) = ⊤_{q}
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. When there are no dynamic assumptions, we avoid mentioning P. 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 will omit the subscript in ⊤_{q} and ⊥_{q}, when it can be inferred by the context. We also implicitely absorb all the irrelevant occurrences of ⊤_{q}.

If D ∈ def(q), we call Not_{D}(D) the D-candidates. Candidates represent the potential negative contribution of each clause: the ‘factual’ part Not_{D}(Q) motivates failure due to clash with the head of D; the remainder Not_{G}(G) expresses failure in the body, if any. Note that the latter only brings the body into what we may call parametric negation normal form, to stress the distinction from classical negation normal form or even from normal form in constructive logics as extension of intuitionism with strong negation. Candidates from each clause in the definition of a predicate need to be considered simultaneously. In fact, if an atom is unprovable from its definition, then its negation must be provable from every D-candidate; symmetrically if it succeeds then its complement must be unprovable from at least one candidate. This is abstractly accomplished by the operator ⊕, which thus works similarly to disjunction. Note that the former is available uniquely as a program constructor and can therefore be used only in the focusing phase of deductions; this allows to preserve the uniformity property. In a second time, when describing the operational semantics of the system, we will show how to ‘compile away’ those disjunctions through an higher-order equivalent of the intersection operator ‘’ described in [?, ?].

Fixed a signature Σ_{P} and given a program P:

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

We abbreviate Not_{D}(def(q)) in def(¬q). If P^{+} is the source program, we use P^{−} for Not_{D}(P^{+}).

Example 1.1 Let def(even) be

even(0) ∧ ΠX:nat. even(ss(X)) ← even(X).

\begin{aligned}M⃗ = N⃗ \\ & & S⊢ ; =^{·} \\ ⊢ & P & M⃗ & =^{·} & N⃗ \end{aligned}  \begin{aligned}M⃗ ≠ N⃗ \\ & S_{≠^{·}}^{⊢} \\ ⊢_{P} M⃗ ≠^{·} N⃗ \end{aligned}
⊢_{P} G_{1} ⊢_{P} G_{2}
S_{∧}^{⊢}
⊢_{P} G_{1} ∧ G_{2}
\begin{aligned}⊢_{P} G_{1} \\ & S_{∨_{1}}^{⊢} \\ ⊢_{P} G_{1} ∨ G_{2} \end{aligned}  \begin{aligned}⊢_{P} G_{1} \\ & S_{∨_{2}}^{⊢} \\ ⊢_{P} G_{1} ∨ G_{2} \end{aligned}
\begin{aligned}D ∈ P ⊢_{P} D >> Q \\ & S_{atm}^{⊢} \\ ⊢_{P} Q \end{aligned}  \frac{I_{⊥}^{⊢}}{⊢_{P}⊥>> Q}

for some t : A ⊢_{P} [t/x]D >> Q

I_{Π}^{⊢}

⊢_{P} Πx : A.D >> Q

\begin{aligned}⊢_{P} D_{1} >> Q \\ & I_{∧_{1}}^{⊢} \\ ⊢_{P} D_{1} ∧ D_{2} >> Q \end{aligned}  \begin{aligned}⊢_{P} D_{2} >> Q \\ & I_{∧_{2}}^{⊢} \\ ⊢_{P} D_{1} ∧ D_{2} >> Q \end{aligned}

⊢_{P} D_{1} >> Q ⊢_{P} D_{2} >> Q

I_{⊕}^{⊢}

⊢_{P} D_{1} ⊕ D_{2} >> Q

⊢_{P} N⃗ =^{·} M⃗ ⊢_{P} G

I\underrightarrow{⊢}

⊢_{P} (G → q N⃗) >> q M⃗

Figure 3: Provability in Horn logic without existentials

Then def(¬even) is:

\begin{matrix}ΠZ:nat. ¬even(s(Z)) ⊕ \\ (¬even(0) ∧ ¬even(s(0)) ∧ ΠX:nat. ¬even(ss(X)) ← ¬even(X). \end{matrix}

Uniform proofs judgments:

⊢_{P} G  Program P uniformly entails G
⊢_{P} D >> Q Clause D immediately entails atom Q under P

We use ⊢_{P^{−}} Not_{G}(G) for Not_{G}(G) = G′ and ⊢_{P^{−}} G′; similarly ⊢_{P^{−}} Not_{D}(D) >> ¬Q for Not_{D}(D) = D′ and ⊢_{P^{−}} D′ >> ¬Q. Theorem 1 (Exhaustivity) Either ⊢_{P^{+}} G or ⊢_{P^{−}} Not_{G}(G). Proof. We generalize this to:

1. Either S^{−} :: ⊢_{P^{+}} G or S^{+} :: ⊢_{P^{−}} Not_{G}(G).

2. I^{−} :: ⊢_{P^{+}} D >> Q or I^{+} :: ⊢_{P^{−}} Not_{D}(D) >> ¬Q.

case

S^{−} = \frac{>> At}{⊥_{Q}>> Q}

Hence by weakening the thesis.

case By the first IH either S^{−} :: ⊢_{P^{+}} G or S^{+} :: ⊢_{P^{−}} Not_{G}(G). By the Partition Lemma M⃗_{1} = M⃗_{2} or there is N⃗ and a substitution θ such that · ⊢ θN⃗ ∈ ∥¬M⃗_{1}∥ and θN⃗ = M⃗_{2}. There are four subcases:

1. S^{−} :: ⊢_{P^{+}} G  By assumption
⊢_{P^{+}} M⃗_{1} = M⃗_{2}  By assumption
⊢_{P^{+}} (q M⃗_{1} ← G) >> q M⃗_{2}  By rule

hence the thesis by weakening

2. S^{+} :: ⊢_{P^{−}} Not_{G}(G)  By assumption
⊢_{P^{+}} M⃗_{1} = M⃗_{2}  By assumption
⊢_{P^{−}} (¬q M⃗_{1} ← Not_{G}(G)) >> ¬q M⃗_{2}  By rule

⊢_{P^{−}} ⋀_{N⃗∈·⊢Not(M⃗)} Π(¬(q N⃗) ← ⊤) ∧ ¬(q M⃗) ← Not_{G}(G) >> ¬qM⃗_{2}

By rule

⊢_{P^{−}} Not_{G}(q M⃗_{1} ← G) >> ¬q M⃗_{2}  By rule Not ←

hence the thesis by weakening

3. ⊢_{P^{+}} G  By assumption
⊢_{P^{+}} θN⃗ = M⃗_{2}  By assumption
⊢_{P^{−}} (¬q θN⃗ ← ⊤) >> ¬q M⃗_{2}  By rule
⊢_{P^{−}} Π(¬qN⃗ ← ⊤) >> ¬q M⃗_{2}  By rule

⊢_{P^{−}} ⋀_{N⃗∈·⊢Not(M⃗)} Π(¬(q N⃗) ← ⊤) ∧ ¬(q M⃗) ← Not_{G}(G) >> ¬qM⃗_{2}

By rule

⊢_{P^{−}} Not_{G}(q M⃗_{1} ← G) >> ¬q M⃗_{2}  By rule Not ←

hence the thesis by weakening

4. ⊢_{P^{−}} Not_{G}G  By assumption
⊢_{P^{+}} θN⃗ = M⃗_{2}  By assumption

as above as the first hypothesis is not used.

case By the second IH ⊢_{P^{+}} D_{1} >> Q or ⊢_{P^{−}} Not_{D}(D_{1}) >> ¬Q and ⊢_{P^{+}} D_{2} >> Q or ⊢_{P^{−}} Not_{D}(D_{2}) >> ¬Q:

1. ⊢_{P^{+}} D_{1} >> Q  By assumption
⊢_{P^{+}} D_{2} >> Q  By assumption
⊢_{P^{+}} D_{1} ⊕ D_{2} >> Q  By rule

hence the thesis by weakening

2. ⊢_{P^{+}} D_{1} >> Q  By assumption
⊢_{P^{−}} Not_{D}(D_{2}) >> ¬Q  By assumption
⊢_{P^{−}} Not_{D}(D_{1}) ∧ Not_{D}(D_{2}) >> ¬Q  By rule

⊢_{P^{−}} Not_{D}(D_{1} ⊕ D_{2}) >> ¬Q  By ruleNot_{D}⊕

hence the thesis by weakening

3. ⊢_{P^{+}} D_{2} >> Q  By assumption
⊢_{P^{−}} Not_{D}(D_{1}) >> ¬Q  By assumption
⊢_{P^{−}} Not_{D}(D_{1}) ∧ Not_{D}(D_{2}) >> ¬Q  By rule
⊢_{P^{−}} Not_{D}(D_{1} ⊕ D_{2}) >> ¬Q  By ruleNot_{D}⊕

hence the thesis by weakening

4. ⊢_{P^{−}} Not_{D}(D_{1}) >> ¬Q  By assumption
⊢_{P^{−}} Not_{D}(D_{2}) >> ¬Q  By assumption
⊢_{P^{−}} Not_{D}(D_{1}) ∧ Not_{D}(D_{2}) >> ¬Q  By rule
⊢_{P^{−}} Not_{D}(D_{1} ⊕ D_{2}) >> ¬Q  By rule

hence the thesis by weakening

case By the second IH ⊢_{P^{+}} D_{1} >> Q or ⊢_{P^{−}} Not_{D}(D_{1}) >> ¬Q and ⊢_{P^{+}} D_{2} >> Q or ⊢_{P^{−}} Not_{D}(D_{2}) >> ¬Q:

1. ⊢_{P^{+}} D_{1} >> Q  By assumption
⊢_{P^{+}} D_{2} >> Q  By assumption
⊢_{P^{+}} D_{1} ∧ D_{2} >> Q  By rule

hence the thesis by weakening

2. ⊢_{P^{+}} D_{1} >> Q  By assumption
⊢_{P^{−}} Not_{D}(D_{2}) >> ¬Q  By assumption
⊢_{P^{+}} D_{1} ∧ D_{2} >> Q  By rule

hence the thesis by weakening

3. ⊢_{P^{+}} D_{2} >> Q  By assumption
⊢_{P^{−}} Not_{D}(D_{1}) >> ¬Q  By assumption
⊢_{P^{+}} D_{1} ∧ D_{2} >> Q  By rule

hence the thesis by weakening

4. ⊢_{P^{−}} Not_{D}(D_{1}) >> ¬Q  By assumption
⊢_{P^{−}} Not_{D}(D_{2}) >> ¬Q  By assumption
⊢_{P^{−}} Not_{D}(D_{1}) ⊕ Not_{D}(D_{2}) >> ¬Q  By rule
⊢_{P^{−}} Not_{D}(D_{1} ∧ D_{2}) >> ¬Q  By rule

hence the thesis by weakening

case By the second IH ⊢_{P^{+}} [t/x]D >> Q or ⊢_{P^{−}} Not_{D}([t/x]D) >> ¬Q:

1. ⊢_{P^{+}} [t/x]D >> Q  By assumption
⊢_{P^{+}} Πx:A. D >> Q  By rule

hence the thesis by weakening

2. ⊢_{P^{−}} Not_{D}([t/x]D) >> ¬Q  By assumption
⊢_{P^{−}} Πx:A. Not_{D}(D) >> ¬Q  By rule
⊢_{P^{−}} Not_{D}(Πx:A. D)  By rule

hence the thesis by weakening

case By the second IH ⊢_{P^{+}} D >> Q or ⊢_{P^{−}} Not_{D}(D) >> ¬Q:

1. ⊢_{P^{+}} D >> Q  By assumption
⊢_{P^{+}} Q  By rule

hence the thesis by weakening

2. ⊢_{P^{−}} Not_{D}(D) >> ¬Q  By assumption
⊢_{P^{−}} Not_{G}(Q)  By rule

hence the thesis by weakening

case By the first IH ⊢_{P^{+}} G_{1} or ⊢_{P^{−}} Not_{G}(G_{1}) and ⊢_{P^{+}} G_{2} or ⊢_{P^{−}}

Not_{G}(G_{2}):

1. ⊢_{P^{+}} G_{1}  By assumption
⊢_{P^{+}} G_{2}  By assumption
⊢_{P^{+}} G_{1} ∧ G_{2}  By rule

hence the thesis by weakening

2. ⊢_{P^{+}} G_{1}  By assumption
⊢_{P^{−}} Not_{G}(G_{2})  By assumption
⊢_{P^{−}} Not_{G}(G_{2}) ∨ Not_{G}(G_{1})  By rule
⊢_{P^{−}} Not_{G}(G_{1} ∧ G_{2})  By rule

hence the thesis by weakening

3. ⊢_{P^{+}} G_{2}  By assumption
⊢_{P^{−}} Not_{G}(G_{1})  By assumption
⊢_{P^{−}} Not_{G}(G_{2}) ∨ Not_{G}(G_{1})  By rule
⊢_{P^{−}} Not_{G}(G_{1} ∧ G_{2})  By rule

hence the thesis by weakening

4. ⊢_{P^{−}} Not_{G}(G_{1})  By assumption
⊢_{P^{−}} Not_{G}(G_{2})  By assumption
⊢_{P^{−}} Not_{G}(G_{2}) ∨ Not_{G}(G_{1})  By rule
⊢_{P^{−}} Not_{G}(G_{1} ∧ G_{2})  By rule

hence the thesis by weakening

case By the first IH ⊢_{P^{+}} G_{1} or ⊢_{P^{−}} Not_{G}(G_{1}) and ⊢_{P^{+}} G_{2} or ⊢_{P^{−}}

Not_{G}(G_{2}):

1. ⊢_{P^{+}} G_{1}  By assumption
⊢_{P^{+}} G_{2}  By assumption
⊢_{P^{+}} G_{1} ∨ G_{2}  By rule

hence the thesis by weakening

2. ⊢_{P^{+}} G_{1}  By assumption
⊢_{P^{−}} Not_{G}(G_{2})  By assumption
⊢_{P^{+}} G_{2} ∨ G_{1}  By rule

hence the thesis by weakening

3. ⊢_{P^{+}} G_{2}  By assumption
⊢_{P^{−}} Not_{G}(G_{1})  By assumption
⊢_{P^{+}} G_{2} ∨ G_{1}  By rule

hence the thesis by weakening

4. ⊢_{P^{−}} Not_{G}(G_{1})  By assumption
⊢_{P^{−}} Not_{G}(G_{2})  By assumption
⊢_{P^{−}} Not_{G}(G_{2}) ∧ Not_{G}(G_{1})  By rule
⊢_{P^{−}} Not_{G}(G_{1} ∨ G_{2})  By rule

hence the thesis by weakening

case The (dis)equality case follows from the decidability of the = judgment to

be detailed later in the unification logic judgment.

□

2 Augmentation

We for now restrict to programs with

• flat parameters:i.e. parameters can occur is assumption only at the toplevel,

• no mutual recursion

• second-order terminating clauses with the simultaneous subterm ordering. Judgments:

• Γ ⊢_{Φ}^{Q} Notα(D): Complementation of the dynamic definitions in D w.r.t. an atom Q and input terms Φ.

• Γ ⊢_{Φ}^{Q} Notα(D): Complementation of assumption D.

• Γ ⊢_{Φ}^{Q} Not^{x}(D): Complementation of assumption D w.r.t. x.

• Γ ⊢_{Φ}^{Q} Not_{i}^{x}(D): Complementation of assumption D w.r.t. x and position i.

• ⊢_{Φ} aug_{D}(D): Augmentation of clause D.

• Γ; D ⊢_{Φ} aug_{G}(G): Augmentation of goal G where,

• Γ is a list of parameters.

• D is a conjuction of assumption.

• Φ is a list of input evars. We can think of assumption complementation, i.e. complementation of clauses

that are by definition parametric in some x, as standard clause complementation w.r.t. x. Informally, for an atomic assumption, say q M_{1} … M_{i−1} x M_{i+1} … M_{n}, its complement can be taken as Not_{D}(q_{x} M_{1} … M_{i−1} M_{i+1} … M_{n}). We have to exercise then some care to reposition the parameter we have pivoted on.

We present two definitions: the first (eager complementation) computes complemetation of ground terms via the auxiliary judgment Γ ⊢_{Φ}^{Q} Not_{i,j}^{x}(D) ⇒ D′, while the second (lazy complemetation) always introduces disequations, even when they are unsatisfiable:

Definition 2.1 (Eager Assumption Complementation) Let for 0 ≤ j ≤ n, Z_{j} be a fresh logic variable of correct type: the judgement Γ ⊢_{Φ}^{Q} Not_{i}^{x}(D) = D′ is realized by the following rules:

head(Q) = q, Σ(q) = \overline{A_{n}} → prop
Not_{i}^{x}⊤

Γ ⊢_{Φ}^{Q} Not_{i}^{x}(⊤_{q}) = ΠZ_{1} :A_{1}…. ΠZ_{n}:A_{n}. ¬q Z_{1} … Z_{i−1} x Z_{i+1} … Z_{n}

p ≢ head(Q)
Not_{i}^{x}At − nmr
Γ ⊢_{Φ}^{Q} Not_{i}^{x}(p \overline{M_{n}} ← G) = ⊤_{q}
Γ ⊢_{Φ}^{Q} Not_{i}^{x}(D_{1}) = D′_{1} Γ ⊢_{Φ}^{Q} Not_{i}^{x}(D_{2}) = D′_{2}
Not_{i}^{x}∧
Γ ⊢_{Φ}^{Q} Not_{i}^{x}(D_{1} ∧ D_{2}) = D′_{1} ⊕ D′_{2}
Γ ⊢_{Φ}^{Q} Not_{i}^{x}(D_{1}) = D′_{1} Γ ⊢_{Φ}^{Q} Not_{i}^{x}(D_{2}) = D′_{2}
Not_{i}^{x}⊕
Γ ⊢_{Φ}^{Q} Not_{i}^{x}(D_{1} ⊕ D_{2}) = D′_{1} ∧ D′_{2}
Γ ⊢_{Φ}^{Q} Not_{i}^{x}(D) = D′
Not_{i}^{x}Π
Γ ⊢_{Φ}^{Q} Not_{i}^{x}(Πy:B. D) = Πy:B. D′
Γ ⊢_{Φ}^{Q} Not_{i,j}^{x}(q \overline{M_{n}}) = D′ Γ ⊢_{Φ}^{Q} Not_{G}(G) = G′
Not_{i}^{x} ←
Γ ⊢_{Φ}^{Q} Not_{i}^{x}(q \overline{M_{n}} ← G) = D′ ∧ ¬q \overline{M_{n}} ← G′

∃j:1 ≤ j ≤ n, j ≢ i . M_{j} ∈ Γ ∪ Φ
Not_{i,j}^{x}Atc

Γ ⊢_{Φ}^{Q} Not_{i,j}^{x}(q \overline{M_{n}}) ⇒ ΠZ_{1} :A_{1}…. ΠZ_{n}:A_{n}. ¬q Z_{1} … Z_{i−1} x Z_{i+1} … Z_{n} ← M_{j} ≠^{·} Z_{j}

∃j:1 ≤ j ≤ n, j ≢ i Not_{i,j}^{x}At

Γ ⊢_{Φ}^{Q} Not_{i,j}^{x}(q \overline{M_{n}}) ⇒ ⋀_{N∈Not(M_{j})} Π(¬q Z_{1} … N … x … Z_{n}) ← ⊤_{q}

where

Γ ⊢_{Φ}^{Q} Not_{i,j}^{x}(D) = ⋀ D′ | Γ ⊢_{Φ}^{Q} Not_{i,j}^{x}(D) ⇒ D′

In the rule Not_{i,j}^{x}At we choose a term M_{j} in the source atom such that it is either an input term or another parameter, in a CLP style, we add the relative disequation. Otherwise we compute its complement with a call to Not. In particular, if M_{j} is an essentially existential variable, its complement is empty and ⊤_{Q} is returned.

Definition 2.2 (Lazy Assumption Complementation) The judgement Γ ⊢_{Φ}^{Q} Not_{i}^{x}(D) = D′ is realized by the following rules:

head(Q) = q, Σ(q) = \overline{A_{n}} → prop
Not_{i}^{x}⊤

Γ ⊢_{Φ}^{Q} Not_{i}^{x}(⊤_{q}) = ΠZ_{1} :A_{1}…. ΠZ_{n}:A_{n}. ¬q Z_{1} … Z_{i−1} x Z_{i+1} … Z_{n}

1 ≤ j ≤ n, j ≠ i Not_{G}(G) = G′
Not_{i}^{x}At

\begin{matrix}Γ ⊢_{Φ}^{Q} Not_{i}^{x}(q \overline{M_{n}} ← G) = ⋀ ΠZ_{1} :A_{1}…. ΠZ_{n}:A_{n}. ¬q Z_{1} … Z_{i−1} x Z_{i+1} … Z_{n} ← M_{j} ≠^{·} Z_{j} \\ ∧ ¬q \overline{M_{n}} ← G′ \end{matrix}

p ≢ head(Q)
Not_{i}^{x}At − nmr
Γ ⊢_{Φ}^{Q} Not_{i}^{x}(p \overline{M_{n}} ← G) = ⊤_{q}
Γ ⊢_{Φ}^{Q} Not_{i}^{x}(D_{1}) = D′_{1} Γ ⊢_{Φ}^{Q} Not_{i}^{x}(D_{2}) = D′_{2}
Not_{i}^{x}∧
Γ ⊢_{Φ}^{Q} Not_{i}^{x}(D_{1} ∧ D_{2}) = D′_{1} ⊕ D′_{2}
Γ ⊢_{Φ}^{Q} Not_{i}^{x}(D_{1}) = D′_{1} Γ ⊢_{Φ}^{Q} Not_{i}^{x}(D_{2}) = D′_{2}
Not_{i}^{x}⊕
Γ ⊢_{Φ}^{Q} Not_{i}^{x}(D_{1} ⊕ D_{2}) = D′_{1} ∧ D′_{2}
Γ ⊢_{Φ}^{Q} Not_{i}^{x}(D) = D′
Not_{i}^{x}Π
Γ ⊢_{Φ}^{Q} Not_{i}^{x}(Πy:B. D) = Πy:B. D′

Note that if M_{j} is essentially existential, we create a unsatisfiable constraint which will simplify in ⊥.

Now collect the result of complementing D w.r.t. x for every position:

Γ ⊢_{Φ}^{Q} Not^{x}(D) = ⋀ Γ ⊢_{Φ}^{Q} Not_{i}^{x}(D) for every i such that x ∈ Q_{|_{i}}

Moreover, we do the same for every parameter which is relevant to the type of q:

Γ ⊢_{Φ}^{Q} Notα(D) = ⋀ Γ ⊢_{Φ}^{Q} Not^{x}(D) for every x:A ∈ Γ such that
if Σ(q) = \overline{A_{n}} → prop, then there is a i such that A_{i} ≡ A

Finally

Γ ⊢_{Φ}^{Q} Notα(D) = ⋀ Γ ⊢_{Φ}^{Q} Notα(def(q, D))

We briefly comment on the rules:

• The rule Not_{i}^{x}⊤ allows to build a new negative assumption w.r.t. q, x, i in case one is not present in the source program. As we have no information at all w.r.t. q, the most general negative assumption is added.

• If instead the atomic assumption considered is different (and later non mutually recursive) to the pivot atom, the trivial clause is added.

• The rest of the rules simply recur on the structure of the assumption.

Remark that there are three-layers: once we have collected the complement of an assumption w.r.t. to x and a given position i, we need to do the same for every other position x can occur in the atom we are complementing with. Once this is done, we proceed to do it again w.r.t. every parameter in Γ whose type (for the time being only of base type) can be used in building argument to the pivot atom. Recall if there are no assumptions returned at all, by convention the result is ⊤_{q}, i.e. the empty conjunction.

We now turn to the judgments to augment a program: ⊢_{Φ} aug_{D}(D) merely recurs on the structure of clauses collecting in Φ a list of imput terms and then calls Γ; 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 Q, x, Γ, D, Φ to assumption complementation.

\frac{aug_{D}⊥}{⊢_{Φ} aug_{D}(⊥) = ⊥}  \frac{aug_{D}⊤}{⊢_{Φ} aug_{D}(⊤) = ⊤}

⊢_{Φ} aug_{D}(D_{1}) = D′_{1} ⊢_{Φ} aug_{D}(D_{2}) = D′_{2} aug_{D}∧

⊢_{Φ} aug_{D}(D_{1} ∧ D_{2}) = D′_{1} ∧ D′_{2}

⊢_{Φ} aug_{D}(D_{1}) = D′_{1} ⊢_{Φ} aug_{D}(D_{2}) = D′_{2} aug_{D}⊕

⊢_{Φ} aug_{D}(D_{1} ⊕ D_{2}) = D′_{1} ⊕ D′_{2}

⊢_{Φ,x:A} aug_{D}(D)
aug_{D}Π
⊢_{Φ} aug_{D}(Πx:A. D) = Πx:A. D′

·; · ⊢_{Φ} aug_{G}(G) = G_{a} aug_{D} ←

⊢_{Φ} aug_{D}(Q ← G) = Q ← G_{a}

Figure 4: Clause Augmentation: ⊢_{Φ} aug_{D}(D) = D′

Example 2.1 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)

Γ ⊢_{Φ}^{Q} Notα(D) = D_{¬}

aug_{G}At

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

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

Γ; (D ∧ D) ⊢_{Φ} aug_{G}(G) = G′ aug_{G} →

Γ; D ⊢_{Φ} aug_{G}(D → G) = D → G′

(Γ, x:A); D ⊢_{Φ} aug_{G}(G) = G′

aug_{G}Π

Γ; D ⊢_{Φ} aug_{G}(Πx:A. G) = Πx:A. G′

Γ; D ⊢_{Φ} aug_{G}(G_{1}) = G′_{1} Γ; D ⊢_{Φ} aug_{G}(G_{2}) = G′_{2} aug_{G}∧

Γ; D ⊢_{Φ} aug_{G}(G_{1} ∧ G_{2}) = G′_{1} ∧ G′_{2}

Γ; D ⊢_{Φ} aug_{G}(G_{1}) = G′_{1} Γ; D ⊢_{Φ} aug_{G}(G_{2}) = G′_{2} aug_{G}∨

Γ; D ⊢_{Φ} aug_{G}(G_{1} ∨ G_{2}) = G′_{1} ∨ G′_{2}

Figure 5: Goal Augmentation: Γ; D ⊢_{Φ} aug_{G}(G) = G_{a}

← Πx:exp. Πy:exp. copy (x y)
→ copy (E x) (F y)

The augmentation procedure calls x, y:exp ⊢^{cp Ex F y} Notα(cp x y), glossing over the context Φ which is not active in this case. First x, y:exp ⊢^{cp Ex F y}

Not_{1}^{x}(cp x y) = (ΠE′: exp. ¬copy E′ y ← x ≠^{·} E′), secondly x, y:exp ⊢^{cp Ex F y}

Not_{2}^{y}(cp x y) = (ΠF′:exp. ¬copy x F′ ← y ≠^{·} F′), yielding:

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

Πx:exp. Πy:exp.

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

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

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

while of course, aug_{D}(cpapp) = cpapp, as enforced by aug_{G}At^{·}. If we had a version of copy without coloring, i.e.

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

→ copy (E x) (F x)

Then we would get the two calls to x:exp ⊢^{cp Ex F x} Not_{1}^{x}(cp x x) = (ΠE′ :

exp. ¬copy E′ x ← x ≠^{·} E′) and x:exp ⊢^{cp Ex F x} Not_{2}^{x}(cp x x) = (ΠF′ :

exp. ¬copy x F′ ← x ≠^{·} F′) and the augmented clause:

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)

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 corrispondent 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. (ΠT:exp. copy x T)
→ copy (E x) F

The call to x:exp ⊢_{Φ}^{inst Ex F} Not_{1}^{x}(ΠT : exp. copy x T) fails as the complement of T is empty [the unsatisfiable clause ΠT : exp. ΠZ : exp. ¬cp x Z ← Z ≠^{·} T] and thus the augmentation is trivial.

Let us see how rule Not_{i}^{x}⊤ enters the picture: consider the open program

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

The judgment x:exp; ⊤_{open} ⊢_{Φ} aug_{G}(open Ex) triggers the rule Not_{i}^{x}⊤, as Σ(open) = exp → prop and thus x:exp ⊢_{Φ}^{open Ex} Not_{1}^{x}(⊤_{open}) = ¬open x:

aug_{D}(oplam) : ΠE:exp → exp. open (lam E) ←
Πx:exp → exp. ¬open x → open (E x)

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

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

Here as term ≢ form, then aug_{D}(isdall) = isdall