A Definitions and Notation

We list some relevant notions^{1}.

Definition A.1 [Terms as trees] Consider ⟨N^{∗}, ·, ∗⟩, the monoid of sequences of natural numbers, called positions with concatenation as the binary operator and the empty sequence as the neuter element. Further, we call a set of positions P ⊆ N^{∗} prefix-closed iff for all p, q, r ∈ N^{∗}: p = q · r ⇒ q ∈ P. For p ∈ P, succ(p) = {q ∈ P | ∃i : q = p · i}. A term t over an signature Σ and an set X of variables is a pair ⟨P, l_{Σ}⟩ satisfying the following conditions:

1. P ⊆ N^{∗} is prefix-closed

2. l_{Σ} : P ⟶ Σ ∪ X

3. If f ∈ Σ and arity(f) = n > 0, then l_{Σ}(p) = f implies that succ(p) = {p · 1, …, p · n}.

Definition A.2 [Contexts] E[F] denotes that the subexpression F inside the brackets has at least one occurrence in E.

Definition A.3 [Linear] A term u is linear if there is no multiple occurrence of the same variable therein. The term θt is called restricted w.r.t. t if either there is x ∈ t such that θx is not linear or there are two distinct variables x_{1}, x_{2} ∈ t such that θx_{1} and θx_{1} share a variable.

Definition A.4 [Universal(Existential) closure]

Definition A.5 [Substitutions]

Definition A.6 [Ground, Instance, Term Subsumption]

Notation A.1 (Tuples and Variables) We write t⃗ for a tuple of elements, in this case terms, whose length is unimportant: \overline{t_{n}} will be used as an abbreviation of t_{1}, …, t_{n}. Note that this notation assumes the properties of finite sets, i.e. x⃗ stands both for x, x′ and x′, x. Further, \overline{x_{n}}, \overline{y_{m}}, \overline{z_{p}} and their vectorized version are intended to stand resp. for tuples (sets) of existential, universal and free variables. They are assumed to be disjoint: \overline{w_{r}} will be used to stand for a tuple of either free or existentially quantified variables. \overline{t_{m}} = \overline{s_{m}} (resp. \overline{t_{m}} ≠ \overline{s_{m}}) will stand for

⋀_{i=1}^{m} t_{i} = s_{i}  ⋁_{i=1}^{m} t_{i} ≠ s_{i}

taking the place sometimes of the more cumbersome notation

\overline{\overline{t_{m}} = \overline{s_{m}}}

. Notation for substitution: [M/x]N.

1under construction

For a syntactic object O, F V (O) will denote the set of its free variables. Discussion of the \underline{U}niversal Query Problem: In Logic textbook a first-order

language usually contains an infinite set of function symbol. On the other hand, the signature of (the language of) a program is finite. in the logic programming community this seemingly innocent issue became hot w.r.t. the semantics of negation-as-failure. Kunen [62] and later Shepherdson [] advocated a return to the former approach which makes the treatment of CET nicer. Afterwards Maher [74] set the records straight (to be continued).

This chapter (III) gives a smooth introduction to first-order disunification: we then show how to cast complement problems as disunification. Thirdly we integrate the latter into (essentially) Sato & Tamaki’s transformation technique. Finally, we deal with the problem of local variables and the related issue of extensional quantification.

B Complement Problems

Complement problems and elimination of negation are not restricted to logic programming , but have some other relevant application in theoretic computer science. Let me refer to [66] and [21] for issues impossible to detail here and for references, keeping in mind that this is just a scratch on the surface of the applications of disunification.

Indeed, complementation problems and variants of the prototypical uncover algorithm proposed in [64] as a first attempt to solve the former, have been studied and tentatively applied in several ways:

• In a functional programming framework, to determine, modulo pattern matching, whether the program clauses describing a function are exhaustive and disjunct, even further to produce a non-ambiguous set of patterns. Moreover it is possible to take advantage of the given sequential application of the rules to provide an improved compiled code. Indeed, if, say, the second rule applies, it means the first one does not: hence the terms reducible by the second rule are in the complement of the LHS of the first

• The connection of complementation to the notion of ground reducibility in term rewriting systems makes it a candidate as a checker for sufficiently completeness [40] of an algebraic (equational) specification. If the latter fails to be complete, the transformation rules my lead to recover the missing cases—hence the motto in [126].

“Stop losing sleep over incomplete specifications”

Here we are looking for counter-examples: if a function is not sufficiently complete, there is a term, built from the constructors in the signature, which is different from any LHS, thus irreducible (see Example 1)

• In term rewriting systems describing infinite transition systems, the complement of a LHS returns the states from which no transition is achievable, providing thusly a tool for the temporal analysis of communicating processes

• In machine learning, a concept can be captured by a term with some (finite) exceptions: the computation of this structure, which is a relative complement, coincides with the search for an explicit representation of the cited concept • Finally, applications to inductive theorem proving under the slogan induc-

tionless induction are under scrutiny.

C Background on First-Order (Dis)Unification

For the sake of this chapter the underlying logical framework is implicitly manysorted. We will disclose the relevant (simple) typing only when it is difficult to infer from the context. We assume thusly that we deal with well-typed objects and rules which preserve this property. We proceed this way for pedagogical reasons only: it would be rather time-consuming to detail each typing in all its glory since it will eventually subsumed by the higher-order framework. Moreover we will not work modulo some (quotient of a) locally free Σ-algebra, but with the standard model, the closed term model, more known to the logic programming people as the Herbrand Universe. See [20, 21] for a presentation respectively modulo many- sorted and Σ-algebrae.

Let E_{ΣT} be the following formulation of CET, Clark’s equational theory, ([17, 62]), that is the equality axioms including congruence (Cng), plus the axioms for finite trees^{2}, also called freeness (or distinctness axioms): for all operators in a signature Σ, Decenforces injectivity, Clh maintains that (the interpretation of) different symbols for function yields different values. Ock should remind of the occur check in the actual unification algorithm. Indeed this theory is the axiomatic and proof-theoretic rendering of the latter algorithm, so that Clark’s Lemma below is referred to as the Unification Lemma. We assume the notational conventions introduced earlier. Definition C.1

(Ref) : ∀(x = x)
(Sym) : ∀(x = y → y = x)
(T rn) : ∀(x = y ∧ y = z → x = z)
(Cng) : ∀(\overline{\overline{x_{n}} = \overline{y_{n}}} → f(\overline{x_{n}}) = f(\overline{y_{n}}))  for all f ∈ Σ
(Dec) : ∀(f(\overline{x_{n}}) = f(\overline{y_{n}}) → \overline{\overline{x_{n}} = \overline{y_{n}}})  for all f ∈ Σ
(Clh) : ∀(f(\overline{x_{n}}) ≠ g(\overline{y_{m}}))  for distinct f, g ∈ Σ
(Ock) : ∀(x ≠ t[x])  if x occurs properly in t[x]

Additionally, define E_{ΣT ∪DCA} (shortened in E_{ΣT^{∗}} or CET^{∗}) as the previous axioms plus

(DCA) : ∀x( ⋁_{f∈Σ} ∃y⃗(x = f(y⃗)))

Theorem 1 (Kunen [62], Maher [74]) If Σ is infinite then E_{ΣT} is a complete theory (for arbitrary sentences); moreover it is a complete axiomatization of the algebra T (Σ) of finite trees. If Σ is finite and not trivial (i.e. it contains at least a constant and a function symbol) the same holds for E_{ΣT ∪DCA}.

2We identify terms and finite trees as usual—the formal definition appears in A.

In fact, E_{ΣT} (or E_{ΣT ∪DCA}) are ℵ_{0}-categorical: the term model (for nontrivial signatures again) is countable, no model is finite as enforced by Clh and Dec and every other denumerable model is isomorphic due to Ock (or Ock and DCA)—see for example Theorem 1 in [77]). Thus completeness of the theory follows by the Los-Vaught theorem.

Theorem 2 (Mal’cev) E_{ΣT} has no finite axiomatization.

It seems again that the crux of the matter lies in the cardinality of the signature, which is in turn related to the universal query problem ??. Finite signatures require the DCA.

The former results are actually corollaries of a theorem by Mal’cev that states that E_{ΣT} is a complete axiomatization of the class of locally free algebrae, i.e. those whose finitely generated subalgebrae are free (this is why the finite trees axioms are called freeness axioms) and that there is a finite axiomatixation of this class. Maher has extended it to finite signatures, rational and infinite trees.

Example 1 The algebra N = ⟨N, 0, s⟩ of naturals is locally free: E_{N^{∗}} contains

(Dec) : ∀x, y, s(x) = s(y) → x = y
(Clh) : ∀x.0 ≠ s(x)
(Ock) : ∀x.x ≠ t[x]  if x occurs properly in t[x]
(DCA) : ∀x.x = 0 ∨ ∃y.x = s(y)

Clh says that 0 is not a successor, Decthat the latter is a one-one mapping, DCA that every non-zero is a successor and the schema Ock that there are no loops, i.e. there are no isolated elements. Note that this signature is the prototypical case where there is an axiomatic redundancy, since every instance of Clh is an instance of Ock. This is to be compared with the usual axiomatization of the numerals. Here the role of Ock is held by Clh and induction, or by the stronger infinitary version of DCA:

(DCA^{ω}) : ∀x.x = 0 ∨ x = s(0) ∨ …
◇

It must be remarked that this formulation of the axioms is not the most economical one, not only due to the formulation of equality but w.r.t. the Ock axiom. In certain circumstances (instances) the latter encompasses the Clhaxiom (see for instance Example 1). Indeed, the logical statement of the occur check is more ample that its operational reading. While it is clear that the axiom should hold only when one side is a variable, it is not clear (to me) whether this is first-order expressible at all^{3}: It may then be argued that the more elegant framework is then rational trees. This does not seem to be the case when disunification is concerned, see [20]. Anyway, we conclude by mentioning the unique solution axiom for rational trees, which replaces Ock, yielding the axioms E_{ΣRT}:

3ELABORATE

US : ∃x∀y : x = t[x] ∧ y = t[x] → x = y for non-trivial t

From Theorem 1 Clark’s lemma follows immediately:

Lemma C.1 (Clark 1978) Let s and t be two terms in T (Σ):

1. if they are unifiable, E_{ΣT} ⊢ ∃(s = t)

2. if not E_{ΣT} ⊢ ∀(s ≠ t)

Note: The lemma holds for any signature, finite or infinite, i.e. it is independent from the DCA. The direct syntactic proof, based on the Martelli-Montanari’s rewrite system, uses only reflexivity^{4} for 1. , congruence plus axioms for finite trees for 2. —the negative result. This contrasts with Lloyd’s proof w.r.t. Robinson algorithm [68]. Proof. Let S be {s = t} and consider the MM-rules augmented with the failure cases (rewriting into ⊥).

Claim C.1

1. If S ⟼_{MM}^{∗} S^{∗} and the latter is in unification solved form, then E_{ΣT} ⊢ ∃(s = t)

2. If S ⟼_{MM}^{∗} ⊥, then E_{ΣT} ⊢ ∀(s ≠ t).

By induction on the number of rewrite steps. □

A very similar, though independent, proof (Unification Lemma) can be found in [112]. Here the author, following [109], gives a neat sequent-style formulation of free equality, which is easily seen provably equivalent to CET. Furthermore he demonstrates cut-elimination for equality formulae. We will implicitly use the latter property when dealing with axiomatic CET in the context of other cut-free (or normalized) systems.

A syntactic proof of Theorem 1 can be achieved by quantifier elimination [74]. This may become handy in the higher-order case, where model-theoretic arguments are less available. On the other hand this result can be obtained from the completeness and termination (and solvability, i.e. the fact that solved forms have solutions, see D.4) of disunification, as proved for instance in [20]^{5}.

4This was, I think, first observed in passing in [98] where the author was refining the MM approach to a meta-logic for unification.

5Actually this directly concerns Σ2-equational formulae but it can easily be extended to arbitrary ones, which is another form, though more limited, of quantifiers elimination.

Moreover the aforementioned proof is achieved w.r.t. a many-sorted language. Since we will be actively interested in designing set of rules for disunification in the higher-order setting, we will consider Theorem 1 as a corollary of future termination and completeness proofs.

Finally, we mention that it is possible to extend the results to rationale and infinite trees, as in the cited papers.

D Equational Problems and Disunification

Disunification is devoted to solving arbitrary first order formulae whose only predicate symbol is equality, call them equational formulae. The definition of what a solution is differs on the application at hand. We may be interested only in the overall validity or in the possible assignments that make the formula valid.

D.1 Related Work

From an historic perspective this field became defined when it was realized by Martelli & Montanari (if not by Herbrand) that first-order -unification can be seen as a transformation on set of equations. On the other hand the work of Mal’cev [75] on the decidability and complete axiomability of the theory of equational algebrae is clearly an ancestor.

The definition of Prolog-II introduced disequation. Indeed Colmerauer [18] showed them to have solutions in the algebra of rational trees. Next Lassez et Marriot [64] proposed the seminal (although awkward) uncover algorithm for computing relative complements. As we will see, those problems are systems of disequation with universally quantified variables.

Kirchner and Lescanne first unified those previous papers in the framework of equational problems and proposed a set of transformational rules, though without a completeness proof [56].

Maher introduced the unification community to Mal’cev’s results [74]. Comon was the first one to present an adequate set of rules [19, 20] and surveyed the field [21]. Now it has become a fast growing area in its own which is impossible to review here: extension of disunification in order-sorted signatures is under research as well as in the presence of specific equational theories, inequalities and symbolic constraints. We will be presenting only what is required for our ultimate goal.

D.2 A Preliminary Account of Disunification

How to go on to derive a disunification procedure can therefore vary from the syntax and semantics we are concerned with, but nevertheless it entails the following steps:

• Provide a set of axioms T that hold in the model we consider

• Design a set of rules R for the transformation of equational formulae that can be proven correct w.r.t. T

• Design a control C on R such that the application of rules satisfying R terminates: irreducible formulae are in solved form and have the same set of solutions of the original problem

• If arbitrary formulae are allowed and solved form are trivially decidable, this entails the decidability and completeness of T .

The simplest example is unification of finite (first-order) trees:

• T is E_{ΣT}

• R are, say, the MM rules; correctness corresponds to the preservation of solutions under rule application, or it can be refined into the content of Clark’s lemma

• Solved forms yield idempotent substitutions (see definition D.7) and control restricts the application of variable elimination. Completeness (of the theory) is established for example as in [74].

We now list some standard definition that will be useful in the sequel.

Definition D.1 [Equational Formula] An Equational formula is an arbitrary first(higher)-order formula, such that ‘ =′ (resp. ‘ =′_{βη}) is its only predicate symbol.

For instance, an unification problem is equivalent to a finite disjunction of equations.

Definition D.2 [System] A system P is defined by the following grammar

P ::= ⊤ | ⊥ | s = t | s ≠ t | P_{1} ∧ P_{2} | P_{1} ∨ P_{2}

It is convenient to choose a normal form for the former notions. Thus we will consider equational formulae to be prenex, where the matrix is in conjunctive normal form. Other normal forms work equally well, provided they are induced by a canonical rewrite system. See Section D.2.1 for more details.

Definition D.3 [Equational Problem] An equational problem E is a Σ_{2}- equational formula, i.e. it has the form ∃\overline{x_{n}}∀\overline{y_{m}} : P, where P is a system.

Equational problems are also known as elementary formulae [21], but we find this terminology misleading.

We will try to use consistently \overline{x_{n}}, \overline{y_{m}}, \overline{z_{p}} respectively for existential, universal and free—sometimes called the unknown of the problem—variables^{6}. These classes are assumed to be disjoint. It will also be convenient to employ \overline{w_{r}} for either a free or an existentially quantified variable.

Definition D.4 [Solutions] A solution σ of an equational problem E is a closed substitution (from the term algebra) such that F V (E) ⊆ Dom(σ) which satisfies the following requirements:

• If E is ⊤, there are no requirements

• If E is ⊥ then no substitution can be a solution

• If E is s = t, then σs and σt are identical

• If E is s ≠ t, then σs and σt are different

• If E is a disjunction d_{1} ∨ ⋯ ∨ d_{n}, then there is some i such that σ_{|F V (d_{i})} is a solution of d_{i}

• If E is a conjunction c_{1} ∧ ⋯ ∧ c_{n}, then for all i σ_{|F V (c_{i})} is a solution of c_{i}

• If E is ∃\overline{x_{n}}∀\overline{y_{m}} : P, then there is a closed substitution θ_{n} such that for all closed substitutions ρ_{m}, σ is a solution of θ_{n}ρ_{m}P.

Again, this definition can be made parametric to any Σ-algebra A, taking as A-solutions the set of A-assignments for the given unknown that satisfy the previous conditions. Let S(E) be the set of solutions for an equational problem E: we write E_{1} ≈_{A} E_{1} for a Σ-algebra A whenever S(E_{1}) = S(E_{2}). If ϕ ≈_{A} ⊤, we write A ⊧ ϕ.

Definition D.5 . A rule R is sound —no new solution—if

E ⟼_{R} E′ ⇒ S(E′) ⊆ S(E)

It is preserving —no lost solution—if

E ⟼_{R} E′ ⇒ S(E) ⊆ S(E′)

A rule is correct if it is both sound and preserving.

We can think of a rule as a 4-tuple ⟨L, R, SC, C⟩, where to the left and right hand side we add a set SC of side conditions to guarantee correctness and completeness and some control conditions C to help with termination. When not concerned with the latter, we will not mention it, simplifying the exposition of the rules.

Rules are chosen so to transform a problem in an equivalent presentation, called a solved form as a solution can be easily extracted from it. More explicitly:

6I am affording myself the luxury of having both free and existential variables to be consistent with the literature.

Definition D.6 [Completeness] A set of rules S for solving equational formulae is complete w.r.t. a notion of solved form Σ—usually a subset of the former—if for any E there is a family F_{i} in Σ-normal form such that the latter are obtained by the former by application of the rules in S and the union of the solution of the F_{i} is the set of solutions of E.

Several types of solved forms can be considered depending on the application see [21]. We give the most useful to our purposes, in decreasing order of generality.

Definition D.7 [Solved Forms] An equational problem E is in parameterless solved form if it contains no universal quantifiers. It is a solved form with constraints^{7} if it has the form

∃x⃗ : ⋀_{i=1}^{m} z_{i} = t_{i} ∧ ⋀_{j=1}^{n} z′_{j} ≠ s_{j}

where x⃗ = F V (t_{1}, …, t_{m}) ∪ F V (s_{1}, …, s_{n}) and the free variables z_{1}, …, z_{m} occur only once in the system—note: this does not apply to the unknown z′_{1}, …, z′_{n}. A unification solved form is a solved form with constraints where no disequation occurs.

For our purposes the latter two will be relevant. Indeed unification solved form is the prototypical basis for any more complex solved form, like basic formulae [21], simple formulae [74], standard formulae [75], substitutions with exceptions [14] and so on.

The disunification rewrite rules are divided in two big chunks:

• Equality rules, i.e. rules which are correct for any equational algebra

• Rules for finite trees over any signature.

We delay the presentation of the complete set of rules with proviso, control and notational conventions to the higher-order case. We just mention that the first group contains Replacement, Universal Quantifier Elimination, Existential quantifier Elimination and Elimination of Disjunctions. The second batch contain Clash, Decomposition, Occur check. A third section would contain rules which are sensitive to the cardinality of the signature. Here we mention only the Explosion rule, which is clearly motivated by the DCA.

We list below the rules relevant to the following examples in their barest form.

We anticipate the following completeness results [20]: the rules R,C,D,O,U,E,ED are complete for definitions with constraints, while the uncover algorithm is complete for unification solved form w.r.t. linear terms.

7Usually called in the literature a definition with constraints.

\begin{aligned}R1 & : & w = t ∧ P [w] & ⟼ & w = t ∧ [t/w]P \\ UE1 & : & ∀y⃗ : P ∧ y ≠ t & ⟼ & ⊥ \\ UE2 & : & ∀y⃗ : P ∨ y ≠ t & ⟼ & ∀y⃗ : [t/y]P \\ Dec & : & f(\overline{t_{n}}) ≠ f(\overline{u_{n}}) & ⟼ & ⋁_{i=1}^{n} t_{i} ≠ u_{i} \\ E & : & ∀y⃗ : P & ⟼ & ⋁_{f∈Σ}(∃x⃗∀y⃗ : P ∧ x = f(x⃗)) \end{aligned}

In R1 w ∉ V ar(t), in UE1, UE2 y ∈ y⃗; in E, P contains a (dis)equation with LHS w and RHS u, where the latter is not a variable and contains a parameter.

Figure 1: Some disunification rules with minimal proviso

D.2.1 Working with Normal Forms

As a matter of fact, there is some latitude in designing a complete set of rules. This depends on several factors: the algebra under consideration^{8}, the notion of solved form in question, the closeness to an algorithmic version and the usage of a normal form for equational problems.

Addressing the latter, it is a well-known phenomenon in rewriting systems that sometimes an applicable rule is disabled when the problem is brought to normal form. This is why completion algorithms are used. There are basically two approaches:

(1) Work modulo Boolean relations without formalizing the context where rules are applied

(2) Electing to keep the problem in a normal form.

The first approach allows to formulate fewer rules and in a more declarative fashion. The other is closer to an algorithm: it entails some Boolean normalization after each application of our rules, i.e. we are implicitly working on the equivalence classes induced by such a (canonical) rewrite system. Hence the rules are tailored to the normal form in question and tend to multiply: for instance we may need this additional rule for decomposition, fit to conjunctive normal form.

Dec3 : P ∧ (f(\overline{t_{n}}) = f(\overline{u_{n}}) ∨ Q) ⟼ P ∧ ⋀_{i=1}^{n}(t_{i} = u_{i} ∨ Q)

Yet this is just half of the story: even normal form cannot avoid wiring in some subset of Boolean pattern matching. For example R1 is applicable to, say, ∀y : z ≠ s(y) ∧ z = 0 only modulo commutativity. On the other hand even the

8This will be immaterial to us, as we restrict to finite trees.

s = s ⟼ ⊤  ¬(s = t) ⟼ s ≠ t
s ≠ s ⟼ ⊥  (ϕ ∧ ψ) ∨ χ ⟼ (ϕ ∨ ψ) ∧ (ψ ∨ χ)
ϕ ∧ ϕ ⟼ ϕ  ϕ ∨ ϕ ⟼ ϕ
ϕ ∧ ⊤ ⟼ ϕ  ϕ ∨ ⊤ ⟼ ⊤
ϕ ∧ ⊥ ⟼ ⊥  ϕ ∨ ⊥ ⟼ ϕ
¬⊤ ⟼ ⊥  ¬⊥ ⟼ ⊤
¬¬ϕ ⟼ ϕ  ¬(ϕ ∧ ψ) ⟼ ¬ϕ ∨ ¬ψ
¬(ϕ ∨ ψ) ⟼ ¬ϕ ∧ ¬ψ  ϕ ∧ (ϕ ∨ ψ) ⟼ ϕ

Figure 2: Rules for normalization

liberal approach of (1) cannot evade taking care of Boolean simplification steps like absorption of neuter elements. Moreover there is the issue of some quantifier manipulation; for instance suppression of empty quantification (resp. universal and existential) can be performed by some explicit rule [20] like Elimination of Parameters and Cleaning, or can be pushed into a wider notion of normal form. The latter could then include prenexing operations as additional rewrite steps. In summary in this chapter we will compromise, following approach (1) in the formulation of the rules and furthermore suppressing mention of logical simplification steps. Moreover we will apply an implicit type discipline in the examples, skipping the rules for many-sorted manipulations.

On the other hand, we now list in Figure D.2.1 the rules which form a canonical system for commutativity, associativity and symmetry of quantifier free equational formulae leading to conjunctive normal form.

We add the rules for empty quantification. Here ‘Q‘ stands for both quantifiers. Remember that normalization applies to formulae already in prenex form. Indeed we are essentially concerned with equational problems.

Qx⃗, x : ϕ ⟼ Qx⃗ : ϕ  x ∉ F V (ϕ)

To be precise, though, we should show that the composition of the two sets still induces a quotient, notwithstanding the latter is a higher-order rewrite system, see [11].

D.3 Term Complement as Disunification

We now address how to express the (relative) complement problem on terms as an equational formula [64] [21]. An open term t can be seen as the intensional representation of its ground instances, say ∥t∥. According to this set-theoretic interpretation, the complement of t is the set of ground terms which are not instances of t, i.e. are not in ∥t∥. It is natural to generalize this to the notion of relative complement; this corresponds to compute a suitable representation of all the ground instances of a given (finite) set of terms which are not instances of another given one, in symbols:

∥t_{1}, …, t_{n}∥ − ∥u_{1}, …, u_{m}∥

where dots represent (set theoretic) union^{9}. More properly

∥t_{1}, …, t_{n}∥ =_{def} ⋃_{i=1}^{n} ∥t_{i}∥

We will assume that any sequence ∥t_{1}, …, t_{n}∥ is without repetition modulo subsumption, i.e. every element is incomparable with everyone else under the subsumption ordering.

Let F V (t_{1}, …, t_{n}) = x⃗ disjoint from F V (u_{1}, …, u_{m}) = y⃗. Then the relative complement problem can be expressed by the following restricted format of equational problem, where the z_{i}’s are free.

∃x⃗∀y⃗ : ⋀_{i=1}^{n} z_{i} = t_{i} ∧ ⋀_{i=1}^{m} z_{i} ≠ u_{i}

With no loss of generality we will take n = 1: indeed:

∥t_{1}, …, t_{n}∥ − ∥u_{1}, …, u_{m}∥ = ⋃_{i=1}^{n}(∥t_{i}∥ − ∥u_{1}, …, u_{m}∥)

which corresponds to

⋀_{i=1}^{n}(∃x⃗_{i}∀y⃗ : z = t_{i} ∧ ⋀_{j=1}^{m} z_{i} ≠ u_{j})

Example 2

ss0 ⟼ 0
y + 0 ⟼ y
0 + y ⟼ y
y + y ⟼ 0

These rules define integer addition modulo 2. The question of sufficient completeness (in this case positive) can be expressed by the following problem (which intuitively leads to ⊥):

∃x_{1}x_{2}∀y : z = x_{1} + x_{2} ∧ z ≠ ss0 ∧ z ≠ y + 0 ∧ z ≠ 0 + y ∧ z ≠ y + y which corresponds to

9Another equivalent notation found in the literature is t_{1} ∨ ⋯ ∨ t_{n} \ u_{1} ∨ ⋯ ∨ u_{m} [64], or a mixture of the two.

∥x_{1} + x_{2}∥ − ∥ss0, 0 + y, y + 0, y + y∥
◇

Then, since a variable stands for the universe of discourse, a complement problem is representable merely by ∥z∥−∥u_{1}, …, u_{m}∥, i.e. a simpler (∃-degenerate) case of equational problem

∀y⃗ : ⋀_{i=1}^{m} z ≠ u_{i}

Thus a disunification algorithm over finite trees will solve complement problems, eventually providing values for free variables^{10}.

We now give an example of disunification on the numerals signature, which shall be required in the synthesis of the odd program. It consists in solving

∀y : z ≠ 0 ∧ z ≠ ssy  (1)

The intuitive solution of (1) is z = s(0), i.e. according to Definition D.4 the substitution [s(0)/z]. We will use the rules in Figure D.2 and gloss over some other rule application, like clashes (sometimes denoted Clh(T ruthV alue) for mnemonic reasons, and elimination of trivial [dis]equations) as well as normalization steps. Branches stemming from the explosion rule are numbered and pursued separately (keeping in mind that they form a disjunction, i.e. a finitely branching tree from a search standpoint). R(x) denote application of the rule R on variable x. Sometimes we use the more informative notation R(s = t).

10Unfortunately the algorithm typically does not preserve the Π_{1}-format, see the Explosion rule.

Example 3

∀y : z ≠ 0 ∧ z ≠ ssy

⟼_{E(z)(1,2)}

(1) ∀y : z ≠ 0 ∧ z ≠ ssy ∧ z = 0

⟼_{R1(z)}

∀y : 0 ≠ 0 ∧ 0 ≠ ssy ∧ z = 0

⟼_{Clh(F)}^{∗} ⊥

(2) ∃x∀y : z ≠ 0 ∧ z ≠ ssy ∧ z = sx

⟼_{R1(z)}

∃x∀y : sx ≠ 0 ∧ sx ≠ ssy ∧ z = sx

⟼_{Dec,Clh(T)}^{∗}

∃x∀y : x ≠ sy ∧ z = sx

⟼_{E(x)(2.1,2.2)}

(2.1) ∃x∀y : x ≠ sy ∧ z = sx ∧ x = 0

⟼_{R1(z)}

∃x∀y : 0 ≠ sy ∧ z = s(0) ∧ x = 0

⟼_{Clh(T)}^{∗} z = s(0)

(2.2) ∃x_{1}x∀y : x ≠ sy ∧ z = sx ∧ x = sx_{1}

⟼_{R1(x),Dec1,UE_{1}(y)}^{∗}

⊥

◇

Formally speaking, our problem has the unification solved form ∃x : z = s(0) ∧ x = 0, but we project away the value for the unknown z which we are interested in^{11}.

Note in the derivation the following typical pattern: application of an explosion is performed as a last resort w.r.t. the elected solved form —for instance, it can be prioritized to eliminate parameters—and immediately accompanied by a replacement of the exploded variable. This may lead to formulate a derived rule combining the above^{12}:

E + R_{(w=f(x⃗))} : ∀y⃗ : P ⟼ [f(x⃗)/w]( ⋁_{f∈Σ} ∃x⃗∀y⃗ : P ∧ w = f(x⃗))

D.3.1 Barbuti’s Not

Compare with the Not algorithm for first-order terms that specializes [64] and is at the heart of Barbuti et al.’s approach [9]. We present it in a typed framework, differently from the original version^{13}.

11It is not clear yet when projection may get troublesome. Furthermore it could be interesting to understand if it is possible to implement the rewriting in a lazy way so as to stop when content with the values for the unknown even before reaching the required solved form.

12It may seem, at first sight, that we substitute w which could be free in P with x which is bound by ∃, so that there is a capture: actually, the proviso on E requires w to be already existential.

Definition D.8 Assume a simple typing for a finitary signature Σ. We define Not(t : τ) by structural induction, where we suppose that t_{i} has type τ_{i}:

Not(x : τ)  = ∅ : τ
Not(f(\overline{t_{n}}) : τ) =
\{g(\overline{z_{p}}) : τ | for all g ∈ Σ distinct from f\} ∪

{f(x_{1}, …, x_{i−1}, s⃗, x_{i+1}, …, x_{n}) : τ | s ∈ Not(t_{i}) : τ_{i}, i ∈ [1, n]}

Standard Prolog is not typed: this means that the uni-sorted version of this function tends to produce a lot of irrelevant outcomes (this has some analogy with the problems raised in in [31]). For example, the result of Not(0) in the (informal) signature of lists of numerals contains not only {s(x)} as expected, but also {nil, 0.nil …}. This may tend to increase dramatically with the size of the signature. On the other hand, fixing

Σ = {0 : nat, nil : nlist, s : nat → nat, cons : nat → nlist → nlist}

for example Not(s(x).nil) yields only the desired {nil, 0.nil, y.z.xs}.

Moreover, more refined type theories, as dependent types and/or subsorts will further constrain the evaluation of Not.

It is possible to prove the set-theoretic correctness of the algorithm.

Proposition D.1 If s ∈ Not(t) then ∥s∥ ⊈ ∥t∥

Proof. By induction on t.

• Basis: trivially true.

• Step: let t ≡ f(\overline{t_{n}}). Proceed by absurdum:

1. s ≡ g(\overline{z_{p}}): hence ∥g(\overline{z_{p}})∥ ⊈ ∥f(\overline{t_{n}})∥ by the Clh axiom.

2. s ≡ f(x_{1}, …, x_{i−1}, t⃗, x_{i+1}, …, x_{n}). Apply the inductive hypothesis to t⃗.

□

The model-theoretic correctness and the usability w.r.t. the transformation technique of the Not procedure is guaranteed by the following result:

Theorem 3 (Barbuti [9]) Let t⃗ be linear, Not(t⃗) = {t⃗_{1}^{c}, …, t⃗_{n}^{c}} and x⃗ a tuple of fresh variables. Then E_{ΣT ∪DCA} ⊧ ∀x⃗(∀(x⃗ ≠ t⃗) ↔ ⋁_{i=1}^{n} ∃(x⃗ = t⃗_{i}^{c})).

13Note anyway that the related notion of covering presented in [12] is many-sorted.

This equivalence is crucial, inasmuch it allows to substitute a complement problems with a set of positive terms. This is actually nothing more than a Corollary of Theorem 4, that we discuss now. Reconsidering Example 1, i.e. the equational problem ∀y : z ≠ 0 ∧ z ≠ s(s(y)) you would expect first to compute Not(0) = {s(x)}, then Not(s(s(y))) = {0, s(0)} and eventually somehow ‘anding’ the result to come up with the expected outcome s(0). This computation is instead executed sequentially inside the transformation technique, as discussed in Section E.3, and for some good reasons. It is worthwhile to imagine the semantics of the ‘anding’ operation. Intuitively, this would consist of some kind of set intersection with unification. This accordingly suggests a framework similar to the lattice of first-order terms ordered by subsumption [65] and modified to take into account disjunction of terms (intensional representation) as urelements. This is pursued in section ??. Well, it turns out that this is not so immediate, due exactly to some undesirable features of the Not operator. In other words, intensional representation of terms are not closed under complementation. One canonical example is as follows: consider the signature {a : i, b : i, f : i → i → i}: intuitively the complement of f(y, y) should look something like:

∥z∥ − ∥f(y, y)∥ ⟼ {a, b} ∪ {f(t, s) | t ≠ s}  (2)

.

Instead, the Not—as well as the uncover—algorithm wrongly outputs:

Not(f(y, y)) = {a, b}

In fact, Lassez & Marriot [64] have shown that the latter are correct only for linear terms: complement of non-linear ones do not have a straightforward finite representation.

This is in our terms the question whether an equational problem correspondent to a complement problem has always an unification solved form. For instance Not(s(0)) = 0 ∨ ssy, yet z ≠ s(0) may be considered irreducible, being already a solved form with constraints. The key problem is then if it is possible to rephrase z ≠ s(0) into a unification problem, i.e. if the relative complement ∥t∥−∥u_{1}, …, u_{m}∥, denoted P_{t;t_{1},...,t_{n}} can be turned in an equivalent unification problem U, so that U ≈_{Σ(T)} P_{t;t_{1},...,t_{n}}. This is answered by:

Theorem 4 ([64]) There is an explicit representations of ∥t∥ − ∥t_{1}, …, t_{n}∥ iff the signature is finite and t_{1}, …, t_{n} are unrestricted w.r.t. t. In particular, let θ_{i} be the mgu of t and t_{i}: then there is a U so that U ≈_{Σ(T)} P_{t;t_{1},...,t_{n}} iff there is ϕ_{i}t such that ∥ϕ_{i}t∥ = ∥θ_{i}t∥ and ϕ_{i}t is unrestricted w.r.t. t for i ∈ [1, n].

Corollary D.1 Let U ≈ P_{t;t_{1},...,t_{n}} and let ∃x⃗∀y⃗ : ⋀_{i=1}^{n} z_{i} = t_{i} ∧ ⋀_{i=1}^{m} z_{i} ≠ u_{i} rewrite to the unification solved form ∃x⃗ : P^{∗}. Then S(U) = S(∃x⃗ : P^{∗})

Again note that the reading of complement problems as equational problems allows a uniform treatment of this kind of examples, namely the former complement problem is equivalent to ∀y : z ≠ f(y, y) which has the solved form z = a ∨ z = b ∨ ∃x_{1}, x_{2} : z = f(x_{1}, x_{2}) ∧ x_{1} ≠ x_{2}.

This constitutes further evidence of the opportunity of rephrasing complements as disunification problems: one point is the ugliness of the original uncover algorithm [64] for intensional complements. The latter, in fact, is fairly complicated, somehow ad hoc, uncooperative to reasoning about it and overall difficult to generalize^{14}. On the other hand, absorbing complements inside disunification offers a neat gain in term of elegance, declaratively, generalizability both to various type-theory and to more complicated syntax. In summary it inherits all the advantages of a sound and fast developing subfield in equational studies. More technically it nicely overcomes the difference between linear and non-linear terms in the difference between various solved forms.

Hence the equivalence between Not and the appropriate disunification problem follows from Corollary ?? : semantically

Corollary D.2 For any ground term s, s ∈ ∥Not(t)∥ iff there exists θ ∈ S(∀y⃗ : z ≠ t) such that s ∈ rng(θ).

Overloading the symbol ‘∨’, the proof-theoretic statement goes like this:

Corollary D.3 Not(t) = t_{1} ∨ ⋯ ∨ t_{n} iff ∀y⃗ : z ≠ t ⟼^{∗} z = t_{1} ∨ ⋯ ∨ z = t_{n}.

As well known, the limitation in D.1 seems to be almost immaterial in logic programming , thanks to the idea of left-linearization introduced by Plaisted and used by Stickel [104, 122] to avoid unnecessary occur checks testing. It simply consists of allowing only heads with linear terms as argument and constraining equal occurrences in the body by a new predicate, say eq, whose definition is eq(x, x). As a matter of fact, this approach is less innocent as it looks at first sight, since it opens the road to transformation of the source program and in particular it sweeps under the rug the move to a touch of constraint logic programming ^{15}.

Anyway, this is not the only road that can be traveled. We may be using:

• Regular tree languages to describe types [35, 101].

• Constrained terms [19]

• Full-fledged disunification (hopefully some neat subset of the rules).

14To moderate this criticism let me mention a efficient parallel version of the aforementioned algorithm [61]

15This is particularly keen to [9] where the source program has a very restricted acceptable format (see Section E.3). Moreover it is consistent with the development of the approach to CLP as in [13]. A discussion can be found in [90].

Both the first and second approaches enjoy closure under complementation. The last one seems to have the right amount of elegance and generality to suit our purposes.

We elaborate a little the second proposal as higher-order logic programming languages are naturally seen as CLP and, irrelatively, there is a connection with the characterization of answer sets initiated in [62]. The idea consists of promoting constraints as in (2) to first class objects; representations (intensional terms) have the form ∥t&c∥ where c is a constraint in a suitable language. More specifically, constraints are conjunctions of non-trivial disequations on the free variables of the constrained term. Thus the relative complement

∥t ∧ d∥ − ∥s_{1} ∧ c_{1}, …, s_{n} ∧ c_{n}∥

is expressed by the equational formula:

∃x⃗∀y⃗ : z = t ∧ d ∧ ¬(z = s_{1} ∧ c_{1}) ∧ … ∧ ¬(z = s_{n} ∧ c_{n})

or, in a more suggestive format

∃x⃗∀y⃗ : z = t ∧ d ∧ (z = s_{1} → ¬c_{1}) ∧ … ∧ (z = s_{n} → ¬c_{n})

Therefore, Example 2 is denoted by

∀y_{1}, y_{2} : z = f(y_{1}, y_{2}) → y_{1} = y_{2}

Comon showed that the class of finite union of constrained terms is closed under complementation. Moreover, we can envision^{16} an extension of this formalism to more expressive constraints, say inequalities. This would make possible the representation of sets of terms which would otherwise require an infinitary notation:

Example 4 [Constrained terms] The set of odd numbers can be represented by both (1) and (2)

∃x∀y : z = s(x) ∧ z ≠ 0 ∧ z ≠ s^{2n}(y) ∧ 0 ≤ n  (3)
∥s(z)∥ − ∥0, s^{2n}(y) | 0 ≤ n∥  (4)

or, with the obvious (I mean introducing abbreviations for the relative equational formulae) abuse of notation, define the odd numbers which are not prime and not included between say 99 and 999.

∃x⃗∀y⃗ : odd(z) ∧ ¬prime(z) ∧ ¬included(99, z, 999)
∥odd(z)∥ − ∥prime(z), included(99, z, 999)∥
◇

16Wishful thinking at this stage: numeric constraints are not accounted for in the formalism.

E Putting it together

We show, through some standard examples, how, given a negation-closed horn program^{17}, we synthesize its complement: the transformation uses some logical equivalences on the completion: moreover the operational semantics is preserved as well, in the sense that the success set of the transformed program coincides with the finite failure set of the source one. This equivalence requirement will probably prove on the practical side to be too stringent: only programs that can be shown to be decision procedures, say through static mode analysis, will be guaranteed to have a complement. For the rest, the responsibility will reside on the user (see the discussion in the Introduction).

First the simplest example.

E.1 Even Example

Consider our favorite program:

                     even(0).
                     even(s(s(Y))) :- even(Y)

Form the completion of the program comp(even) and massage it so as to derive its complement odd as in Figure E.1:

Clearly most of the label on the ⇝ rewrite relation are self-explanatory. It is nevertheless worthwhile to state specifically the lift equivalence in its generality. Recall that \overline{y_{m}} are the new variables renaming the definiendum, while \overline{x_{n}} are now the local ones. If k = 0 then the rewriting is the identity, since the RHS converts to false.

Definition E.1 Lift

∀\overline{y_{m}}(∀\overline{x_{n}}(\overline{y_{m}} ≠ \overline{t_{m}}[\overline{x_{n}}] ∨ ⋁_{i=1}^{k} ¬p_{i}[\overline{x_{n}}])) ↔

∀\overline{x_{n}}(\overline{y_{m}} ≠ \overline{t_{m}}[\overline{x_{n}}]) ∨ ⋁_{i=1}^{k} ∃\overline{x_{n}}(\overline{y_{m}} = \overline{t_{m}}[\overline{x_{n}}] ∧ ¬p_{i}[\overline{x_{n}}])) )

Remark E.1 (Lift correctness) The lift equivalence follows classically from E_{ΣT} (and E_{ΣRT}). In particular the derivation employs congruence and decomposition axioms in each sense and classical manipulation of connectives and quantifiers^{18}. In particular it does not use DCA.

17We call negation-closed a horn program such that it is closed under complementation, i.e. it is equivalent to one whose complementation is still horn. Non-negation closed programs are treated in Section F, when dealing with universal quantification

18On the other hand, CET is decidable, so why bother.

∀x.even(x) ↔ x = 0 ∨ ∃y.x = ss(y) ∧ even(y)

⇝_{cp}

∀x.¬even(x) ↔ ¬(x = 0 ∨ ∃y.x = ss(y) ∧ even(y)) ⇝_{nnf}

∀x.¬even(x) ↔ x ≠ 0 ∧ (∀y.x ≠ ss(y) ∨ ¬even(y)) ⇝_{lift}

∀x.¬even(x) ↔ x ≠ 0 ∧ ∀y.x ≠ ss(y) ∨ (∃y.x = ss(y) ∧ ¬even(y)) ⇝_{dnf}

∀x.¬even(x) ↔ (x ≠ 0 ∧ ∀y.x ≠ ss(y)) ∨ (x ≠ 0 ∧ ∃y.x = ss(y) ∧ ¬even(y)) ⇝_{disunify(x≠0∧∀y:x≠ss(y))}

∀x.¬even(x) ↔ x = s(0) ∨ (x ≠ 0 ∧ ∃y.x = ss(y) ∧ ¬even(y)) ⇝_{disunify(x≠0∧∃y:x=ss(y))}

∀x.¬even(x) ↔ x = s(0) ∨ (∃y.x = ss(y) ∧ ¬even(y)) ⇝_{prettyp}

                     odd(s(0)).
                     odd(s(s(Y))) :- odd(Y).

Figure 3: odd example

As we said earlier, the linearity condition guarantees that the disunification process ends in an unification solved form (Definition D.7), but it is no restriction, as the next example shows. What we may end up with is a solved form with constraints, which in this case are simply disequations on the (many-sorted) Herbrand universe.

Example 5 Consider the usual program for membership in lists:

                  member(X,X.XS).
                  member(X,Y.YS):- member(X,YS).

Its completion is

∀z, zs(member(z, zs) ↔ ∃x, xs(zs = x.xs ∧ z = x) ∨
∃x, y, ys(zs = y.ys ∧ z = x ∧ member(x, ys)))

Now the transformation: note that we have to choose zs rather then z as the variable to explode in the same disjunct. In general it is not clear whether this choice that happens to be compelled in this circumstance by the side conditions of the rule can be supported by some kind of experimental heuristics^{19}. Remark anyway that the implicit type-discipline considerably reduces this search. The computation is reported in Figure 5 tacitly restricting the solved form to contain only the appropriate variables^{20}.

19This naturally leads to a form of nested OR-parallelism, [61], entailing pursuing at the same times branches produced by explosion, as well as explosion on other variables.

Remark again that since the starting problem was nonlinear, the solved form contains a constraint. ◇

E.2 To be completed

At this point we sum up the procedure: Let p be a n-ary predicate and suppose there are m clauses of the form p(…) in the underlying program, where the i − th clause has the following form

p(t_{i,1}[y⃗], …, t_{i,n}[y⃗]) ← B_{i,1}[y⃗], …, B_{i,k(i)}[y⃗]

for each i, i.e. every clause in the definition, k(i) denotes the number of literals therein, while all the variables occurring in the definition are taken from the set y⃗. Then its completion comp(p) is

∀\overline{x_{n}}(p(\overline{x_{n}}) ↔ ⋁_{i=1}^{m} ∃y⃗( ⋀_{j=1}^{n} x_{j} = t_{i,j}[y⃗] ∧ ⋀_{j=1}^{k(i)} B_{i,j}[y⃗]))

which can be abbreviated in the definiens formula

∀\overline{x_{n}}(p(\overline{x_{n}}) ↔ D[x⃗])

Then the procedure yielding the complement p^{c} of the predicate definition p is obtained thru the following transformation on the definiens formula:

• contraposition (cp)

• conversion into negation normal form (nnf)

• conversion into disjunctive normal form (dnf)

• call of the disunification algorithm (disunify(…))

• lifting of the RHS: see above.

Finally prettypp renames negated atoms into positive ones and performs the inverse of the completion formation procedure, somehow projecting the constraints nicely. We do not consider it an official part of the main transformation, but as a post-processing phase as completion formation is a pre-processing one.

The procedure can be iterated on a whole program. Following [110], it can be shown that:

Proposition E.1 [Sato & Tamaki] P^{c} is the dual of P, i.e. F_{P} = M_{P^{c}}. comp(member) ⇝_{cp}

20This may sweep under the rug a serious constraint projection problem, i.e. which inequalities are to be taken into account for the final format. In this case they are the one for which linearity does not hold: is that heuristics or a satisfactory condition?

∀z, zs(¬member(z, zs) ↔  ∀x, xs(zs ≠ x.xs ∨ z ≠ x) ∧
∀x, y, ys(zs ≠ y.ys ∨ z ≠ x ∨ ¬member(x, ys))

⇝_{lift}

∀z, zs(¬member(z, zs) ↔  ∀x, xs(zs ≠ x.xs ∨ z ≠ x) ∧
∀x, y, ys(zs ≠ y.ys ∨ z ≠ x) ∨
∃x, y, ys.(zs = y.ys ∨ z = x) ∧ ¬member(x, ys)

⇝_{dnf}

∀z, zs(¬member(z, zs) ↔  (d1) ∀x, y, xs, ys.(zs ≠ x.xs ∨ z ≠ x) ∧ (zs ≠ y.ys ∨ z ≠ x)
(d2) ∀x, xs, (zs ≠ x.xs ∨ z ≠ x) ∧
∃x, y, ys.(zs = y.ys ∧ z = x) ∧ ¬member(x, ys)

(d1) ⟼_{E+R(zs=nil)(1.1)}

(d1.1) ∀(nil ≠ x.xs ∨ z ≠ x) ∧ (nil ≠ y.ys ∨ z ≠ x) ∧ zs = nil

⟼_{Cl(T)^{∗}}

zs = nil

⇝_{prettyp}

                              nonmember(X, nil)

(d1) ⟼_{E+R(zs=w.ws)(1.2)}

(d1.2) ∃w, ws∀x, y, xs, ys.(w.ws ≠ x.xs ∨ z ≠ x) ∧
(w.ws ≠ y.ys ∨ z ≠ x) ∧ zs = w.ws

⟼_{UE2(x,y,xs,ys)}^{∗}

∃w(w ≠ z)

⇝_{prettyp}

⟨⟩

(d2) ⇝_{disunify(∀x,xs(zs≠x.xs∨z≠x))} ⟼_{UE2(x,y,xs,ys)}^{∗}

x ≠ y ∧ ∃y, ys.zs = y.ys ∧ z = x

⟼_{norm}

∃y, ys(zs = y.ys ∧ z ≠ x)

⇝_{prettyp}

                              nonmember(X, Y.YS) : −X ≠ Y, nonmember(X, YS).

Figure 4: Synthesis of the nonmember predicate

E.3 Comparison

Note the balance with Barbuti approach: there you start with a specific format in the source program called flat, which includes left-linearization (e) and localization (d); this amounts to simplify the logical complexity of the completion formula and to permit to use the simpler Not algorithm instead of full disunification. We here give their version of the process and reexamine some examples. Let us be more specific: a flat definite program has the following format:

(a) eq(x, x)
(b) p(x⃗) ← q_{1}(x⃗), …, q_{n}(x⃗)
(c) p(x⃗) ← q_{1}(x⃗); …; q_{n}(x⃗)
(d) p(x⃗) ← q(x⃗, y⃗)
(e) p(t⃗) ← q(t⃗^{∗})  var(t⃗^{∗}) ⊆ var(t⃗)

where t⃗ is linear. We gloss over the eight steps necessary for the transformation and the heuristics required to keep the size of the program manageable. The target program is logically equivalent to the source one: the main characteristics of the new program are as follows;

• all predicates are defined by a single clause

• all clauses, but eq(x, x) are linear

• if the body contains a local variable it must occur in a single atom as in (d)

• if a head contains non-variable terms, the body must be a single literal under proviso (e)

• if a body is a conjunction (disjunction) every element is positive and have the same variable of the head.

Example 6

              member(Z,ZS)  :-  m1(Z,ZS) ; m2(Z,ZS).
              m1(X,Y.XS)    :-  eq(X,Y).
              m2(X,Y.YS)    :-  member(X,YS).

              eq(X,X).

◇

Note that the member predicate is almost a best-case scenario, since it is already in the (e) format, so its flat version results only from left-linearization and folding. We give here the flat version of the naive reverse program to show how little of the original format is preserved.

Example 7

       rev([],[]).

       rev(X.XS,R)           :-  rev(XS,Tmp),

                                 append(Tmp, [X], R).
       append([], XS,XS).

       append(X.XS,YS,X.ZS)  :-  append(XS,YS,ZS).

Next the flat versions, with the clauses for rev annotated with the em flat condition:

rev(ZS,YS)          :-  r1(ZS,YS);                      (c)

                         r2(ZS,YS).

r1([],[]).                                               (e)
r2(X.XS,R)          :-  rr2(X,XS,R).                    (e)
rr2(X,XS,R)         :-  rrr2(X,XS,R,Tmp).               (d)
rrr2(X,XS,R,Tmp)    :-  r21(X,XS,R,Tmp),                (b)

                         r22(X,XS,R,Tmp).

r21(X,XS,R,Tmp)     :-  rev(XS,Tmp).                    (e)
r21(X,XS,R,Tmp)     :-  append(Tmp,[X],R).              (e)
append(X,Y,Z)       :-  append1(X,Y,Z);

                         append2(X,Y,Z).

append([],Y,Z)      :-  eq(Y,Z).
append2(X,Y,Z)      :-  append3(X,Y,Z),append4(X,Y,Z).
append3(X.Y,Z,V.W)  :-  eq(X,V)
append4(X.Y,Z,V.W)  :-  append(Y,Z,W).

◇

Given the de-structuring due to the flat format, the constructed completion is simpler and stepwise built as imagined.

\begin{matrix}(a) & ∀x, y.eq(x, y) ↔ x = y \\ (b) & ∀x⃗.p(x⃗) ↔ q_{1}(x⃗) ∧ ⋯ ∧ q_{n}(x⃗) \\ (c) & ∀x⃗.p(x⃗) ↔ q_{1}(x⃗) ∨ ⋯ ∨ q_{n}(x⃗) \\ (d) & ∀x⃗.p(x⃗) ↔ ∃y⃗.q(x⃗, y⃗) \\ (e) & ∀y⃗.p(y⃗) ↔ ∃x⃗.y⃗ = t⃗ ∧ q(t⃗^{∗}) \end{matrix}

Then, it is negated and lifted as expected. Using Theorem 3 universal inequalities stemming from (e) are replaced with their solutions given by the Not algorithm, yielding:

∀y⃗p^{c}(y⃗) ↔ ⋁_{i=1}^{n} ∃x⃗(y⃗ = t⃗_{i}^{c}) ∨ .∃x⃗.y⃗ = t⃗ ∧ q^{c}(t⃗^{∗})

which eventually leads to n facts p^{c}(t⃗_{i}^{c}) and a rule p^{c}(t⃗) : −q^{c}(t⃗^{∗}). To recover some sense in the resulting set of clauses, unfolding is used. It is worthwhile to stress again that the inequalities are computed ‘sequentially’, i.e. independently, due to the mentioned issue of the ‘conjunction’ of intensional terms and that left-linearity is essential for the method to be applicable. Second, it is the unfolding which makes ‘parallel’ the term complementation.

We do not dare to exemplify the method on the rev predicate, hence, back to the odd one:

Example 8

             even(Z)         :-  even1(Z) ; even2(Z).

             even1(s(0)).

             even2(s(s(X)))  :-  even(X).

The negated completion is

neven(x) ↔ neven1(x) ∧ neven2(x)

neven1(x) ↔ ∃z.x = s(z)  from x ≠ 0
neven2(x) ↔ x = 0 ∨ x = s(0) ∨ ∃z.x = s(s(z)) ∧ neven(z) from ∀z.x ≠ s(s(z))

Which eventually yield the clauses:

                 neven(Z)         :-  neven1(Z),

                                       neven2(Z).
                 neven1(s(X)).
                 neven2(0).
                 neven2(s(0)).

                 neven2(s(s(X)))  :-  neven(X).

Only after partial evaluation our good old program reappears. Note that it is difficult to attach an operational, as well as declarative, meaning to the intermediate code. ◇

Unfortunately this is not the end of the story: it remains to deal with the transformation of eq, which, as it stands, cannot be addressed in the given framework. Yet, since this predicate is non-linear it requires an ad hoc treatment, namely for every type^{21} adding the clauses, for every argument position 1 ≤ i ≤ n:

neq(g(\overline{X_{n}}), f(\overline{Y_{m}})).  for distinct f and g
neq(g(\overline{X_{n}}), g(\overline{Y_{n}})) ← neq(X_{i}, Y_{i})  for i ∈ [1..n]

Moreover, the instantiation to variables in open negative literals in what used to be the pre-transformation queries is exactly yielded by the neq predicate. Moreover its operational behavior is not satisfactory: consider the goal neq(XS, X.XS). While it should succeed without bindings, it loops. Clearly, the disunification approach allows a symmetric treatment. It is not a coincidence that more recent version of intensional negation are situated in a constraint framework [13].

21An untyped approach would be unfeasible.

Finally the intermediate code for the member predicate:

   nonmember(X,XS)     :-  nonmember1(X,XS) , nonmember2(X.XS).

   nonmember1(X,[]).

   nonmember1(X,Y.YS)  :-  neq-el(X,Y).

   nonmember2(X,[]).

   nonmember2(X,Y.YS)  :-  nonmember(X,YS).

   neq([],Z.ZS).
   neq(Z.ZS,[]).

   neq(X.XS,Y.YS)      :-  neq-el(X,Y),neq(XS,YS).

Again, partial evaluation with suspension (delaying) of neq yields the wellknown program. The notation ‘neq-el’ alludes to the inequality theory induced by the type of the element of the list which has to be added.

F The Trouble with Local Variables

This section could also be entitled ‘What has universal quantification to do with the negation technique ?’

Answer: even starting with a Horn program, the transformed one may contain universal quantification in the body, stemming from local variables. Consider a program for (irreflexive) transitive closure of a relation, which keeps also track of the intermediate elements in the path construed, in the version of [12]^{22}:

Example 9

          path(X,Y)        :-  path3(X,Y,ZS)
          path3(X,Y,[])    :-  edge(X,Y).
          path3(X,Y,Z.ZS)  :-  edge(X,Z), path3(Z,Y,ZS).

          edge(a,b).
          edge(b,c).

The complement of the program follows:

22Why, you would ask, complicate one’s life with a third argument: well the clue is: consider the (d) clause in flat programs.

        nonpath(X,Y)        :-  all ZS. nonpath3(X,Y,ZS).
        nonpath3(X,Y,[])    :-  nonedge(X,Y).
        nonpath3(X,Y,Z.ZS)  :-  nonedge(X,Z).
        nonpath3(X,Y,Z.ZS)  :-  nonpath3(Z,Y,ZS).

        nonedge(a,c).
        nonedge(b,b).
        nonedge(X,a).
        nonedge(c,X).

◇

This raises several important questions:

1. What is the operational reading of universal quantification in this setting

2. How it mingles with generic judgments (discussed in Section F.1) ?

3. How can this be reflected in the theory of inductive definitions [1] (discussed in ??) ?

This section is devoted to addressing the first one. We start asking the naive query ← nonpath(c, c), with the intuitive reading that indeed it should succeed since the graph is irreflexive. Thus the subgoal ← ∀^{e}ZS.nonpath3(c, c, ZS) should eventually succeed. Nevertheless a naive exhaustive search would loop, since there are infinite paths between c and c in the (cyclic) antigraph.

We thus turn to the literature [77, 12, 50].

F.1 Logic Programming and Universal Quantification

Similarly to implication, several attempts to allow universally quantification in goals in a controlled way were proposed in the mid 80’s (see NQ-Prolog [33], NI [34], clausal intuitionistic logic [78]): They all showed, as far as I am concerned, an amazing amount of technicalities, restrictions, lack of clear operational semantics and mostly the absence of a programming language significance, which is the original sin of all dead languages^{23}.

A possible source of misunderstanding was perhaps the confusion between what we now know as the intensional [81] vs. extensional [9] interpretation of ∀, as well as the implicit assumption of the Closed World Assumption (CWA). This is connected with what has come to be known as the universal query problem [6, 62], discussed in Chapter A^{24}.

23To alleviate this, I have to mention that the impetus to develop NQ-Prolog was the attempt to formalize the British Nationality Act; yet this hardly qualifies as a development of programming languages feature.

24This section must be updated: we need to consider also partial predicates [130].

• Extensional:

∀^{e}x.G holds if for all closed terms t, [t/x]G holds

• Intensional:

∀^{i}x.G holds if for a new parameter a, [a/x]G holds.

We will use the notation Π for the latter, for reasons that will become apparent in the sequel. This dichotomy is also characterized as the difference between the model and proof-theoretical approach.

There is a not so obvious relation^{25} with what we intend the domain of computation to be (recall that in the logic programming tradition this is central to define the intended term model).

• Closed Domain:

the signature is fixed once and for all as the one underlying the program; this is enforced by the DCA, the first-order approximation of the CWA

• Open Domain:

the signature is taken to be infinite; in operational terms this means that it is free to expand during execution by parameters^{26}.

This has some relevant model-theoretic consequences that we may not pursue here (see Theorem 1 in [77]). At the risk of being trivial we instead give the following:

Example 10 Consider the “program” q(a); the query ∀^{e}x.q(x) follows logically from P ∪DCA (in every normal model—this will be assumed from now on) and should accordingly succeed; symmetrically Πx.q(x) does not and it fails, as it should. Yet take the slighter more complicated program:

\begin{matrix}p(0) \\ ∀x.p(s(x)) \end{matrix}

the query ∀^{e}x.p(x) apparently fails to terminate even it follows logically from P ∪ DCA and every instance p(s^{n}(0)) is provable. The query Πx.q(x) still fails.

◇

Before rushing to declaring the intensional approach the obvious winner, let me point out the following:

1. It does not seem at the Horn level to be a problem of classical versus constructive logic; the above derivations exists in the minimal predicative calculus with equality^{27} and DCA. For finite signatures, it is a question of taste to take DCA as a constructive principle. Infinite ones do not arise because they conflict with the Closed Domain Assumption. Even OWA signatures stay finite w.r.t. terminating computations.

25To be further discussed

26I assume at this point that parameter introduction is consistent with CET. Everything should boil down to adding/dropping the DCA. Infinite languages and parameter introduction could be orthogonal.

2. The issue of choice of domain is strongly linked to (constructive) negation: going back to the first example above: a query of the type ← ∃x.¬q(x) could succeed in the Open Domain with answer something like x ≠ b, for a new parameter b. Yet it is not fair to consider constructive negation in the Open Domain as something already given.

There is no contest that intentional quantification has proved to be a really novel and useful language feature: Miller has made a convincing case for its usage to implement local declarations and abstract data types in λProlog; furthermore the Π operator in Elf is the cornerstone of allowing hypothetical and parametrical judgments. Nevertheless it seems that the only reasonable interpretation of universal quantification originating from local variables is an extensional one^{28}. Coming back to Example 9, you may check that the intensional version of ← ∀ZS.nonpath(X, Y, ZS) makes no sense. Note that we have so far carefully avoided to discuss an interpreter for extensional quantification. This is not a coincidence. Barbuti’s first solution is eminently operational, cryptic and incomplete too. Namely, for a predicate q and its complement q^{c}, a query ← ∀yq^{c}(x, y) succeeds whenever:

1. ← q^{c}(x, y) is computed producing a candidate substitution θ

2. ← q(θx, z) fails finitely, for z fresh.

You may indeed check that the query ← nonpath(c, c) succeeds, ← nonpath(b, X) yield answers X = b, X = a and ← nonpath(a, c) fails. The idea seem to use the knowingly mistaken interpretation that NF gives to quantifier in non-ground queries (see Introduction ??) to achieve the result. The source of incompleteness can be localized to the interaction between local variables and conjunction, namely the candidate substitution may be too general to yield the desired finite failure (see example at pp. 213–214 in [9]). Indeed the procedure has to be further factorized as follows:

• If ← q(θx, z) has only finite failure derivations, then succeed

• otherwise further instantiate θx and go to the previous step.

This instantiation is achieved by a procedure herbrand which enumerates the term model. Of course, when dealing with an infinite universe, the procedure always diverges, as admitted by the authors (pp. 226). Hence:

27More precisely with the congruence axiom for the mentioned predicates, see the R1 rule in Section D.

28This interpretation may also be useful in a Datalog sense [69, 70].

“… It is meaningless to talk about the finite failure of SLDN”

Indeed, a clever usage of the DCA may alleviate this problem as explained in [90] and reported in Section F.3.

Nevertheless, we thus agree w.r.t. regarding the overall unfeasibility of this approach, as unable to grant completeness. Therefore we abandon this problematic generate-and-test approach and turn to the refinement of extensionality that goes under the name of proof by case analysis, shortened in CASE. [77, 12] (and somehow also [50]), which is naturally suggested by the second program quoted in Example 10.

CASE is based on two pillars: the idea of term covering [77], i.e. an intensional finite representation of all the ground instances of a term, and on the operational reading of an opportune instance of (an equivalent of) the DCA.

To give the idea away, the point is to prove a positive universal statement by proving a finite set of its instances which nevertheless constitute a covering of the original one.

We will next quote the model-theoretic results which support this new kind of rule. We will also mention the stronger completeness result that can be achieved for SLD and NF . We stress again that the reference theory we are using is the completion of the program plus CET enriched of the DCA. Moreover the latter can be shown to be a conservative extension of Clark’s completion w.r.t. universal positive queries.

F.2 Covering

Recall the relation of subsumption among (typed) first-order terms ?? and related definitions. Note also the following trivial property:

s ≤ t entails ∥s∥ ⊆ ∥t∥

From there we introduce the notion of covering of a term, i.e. a set of terms such that every ground instance of the latter can be obtained as a ground instance of a term in the former. We assume a fixed signature with appropriate kind and type declarations.

Definition F.1 Let t : τ and ξ = {t_{1}, …, t_{n}, …} be a possibly infinite set of terms of the same type. ξ is said to be a covering for t (sometimes denoted t_{1}, …, t_{n}, …, /t) if ∥t∥ ⊆ ⋃_{i∈ω} ∥t_{i}∥. It is exact if ∥t∥ = ⋃_{i∈ω} ∥t_{i}∥. It is tight if no element is an instance of another, i.e. it is an antichain under term subsumption. A partition of t is a disjoint and exhaustive union of the ground instances of t. If t : τ is a variable, then a covering ξ is called a type covering or τ-covering. A τ-covering is canonical if it consists of the type constructors, denoted δ(τ). A covering ξ for t is trivial if ∃t_{i} ∈ ξ : t ≤ t_{i}; in particular, a type covering is trivial if the variable belongs to the cover^{29}.

Example 11 Consider the signature of numerals: x ∨ 0, 0 ∨ sx, ω are resp. a trivial, the canonical and an infinite nat-covering. Consider sx: s0 ∨ ssx, ssy ∨ x, 0 ∨ s0 ∨ ssy, s0 ∨ sss0 ∨ ssx are resp. an exact, a trivial, a non-exact, and an non-tight exact coverings. ◇

While it is clear how to generalize Definition F.1 to tuples of terms, we shall consider them as special single terms with a tuple prefix constructor.

We now list some basic properties of coverings:

Property F.1 A partition of t is an exact and tight covering for t.

Proof. Tightness entails disjointness, exactness exhaustivity. □

We extend the definition of canonical covering to any term in the obvious manner, i.e. we consider δ(τ) as a substitution acting on the free variables of the term.

Property F.2 A canonical covering of t is a partition of t.

We note the following:

Lemma F.1 If ξ = {t_{1}, …, t_{n}, …} is a non-trivial exact covering for t, then for every i , t_{i} < t.

29In this discussion we are implicitly considering terms modulo renaming.

Proof. Exactness entails for all i , t_{i} ≤ t; by non-triviality t_{i} < t. □

A term t : τ induces a set of coverings Ξ_{t:τ}, which can be ordered by a variant of the clause subsumption ordering: Namely:

Definition F.2 For ξ_{1}, ξ_{2} ∈ Ξ_{t:τ}, we say that ξ_{1} ≤ ξ_{2} iff there is a (well-typed) substitution θ s.t. θξ_{1} ⊆ ξ_{2}.

This ‘lattice’ notation stresses similarity with subsumption.

Example 12

(0 ∨ sx) ≤ (0 ∨ s0 ∨ ss0 ∨ sssy)
◇

It is clear that this relation is a partial ordering among coverings.We may thusly introduce posets for a given generator, that is the covered term.

The following lemma allows us to restrict only to posets of type coverings: it easily follows from the definition of covering.

Lemma F.2 Let ξ be a τ-covering and t so that t = θx. Then there exists a covering ξ^{θ} for x so that t_{1}, …, t_{n}, …, /t iff t_{1}^{θ}, …, t_{n}^{θ}, …, /x and for all open t_{i}: t_{i} = θt_{i}^{θ}.

Property F.3 A tight type covering is non-trivial and exact.

Proof. It is exact by definition of type-covering. If it were trivial, it would contain a variable. □

Corollary F.1 A tight type-covering is a partition.

Corollary F.2 A canonical covering δ(τ) is the minimum non-trivial τ-covering.

Proof. Note that a canonical covering is a partition. Furthermore, any smaller covering would be trivial. □

Since we will consider only non-trivial tight coverings, when not partitions, we may form the pointed poset (ppo) ⟨Ξ_{x:τ} , δ(τ), ≤⟩, where δ(τ) is the minimum element of the poset.

In particular the ppo ⟨Ξ_{:τ} , δ(τ), ≤⟩ of tight type coverings is, under this ordering, a chain; besides only one substitution, determined by δ(τ) induces the comparison for every pair of terms. Therefore the ppo ⟨Ξ_{:τ} , δ(τ), ≤⟩ is trivially a lattice, where the top is the type enumerated by x glb and lub are predecessor and successor functions on chains—see ?? for a more general treatment. For usage in the next section (F.3), we thus introduce a decoration of the aforementioned ordering, namely the numbered subsumption ordering.

Definition F.3 Let ⟨Ξ_{:τ} , δ(τ), ≤⟩ be the chain of tight type coverings: then ξ ≤_{1} ξ′ iff ξ′ = succ(ξ) iff lub(ξ, ξ′) = ξ′. Let ≤_{n+1} be the n-th iteration of this relation. Define the case-rank of a covering cr(ξ : τ) = n : δ(τ) ≤_{n} ξ.

We now address the model theoretic foundations for coverings and the CASE rule for the Horn case, by referring to some results proved in [77] for the unisorted case, but holding for the mani-sorted one too.

First it is shown that finite type coverings do cover the domain of every model of CET^{∗}.

Proposition F.1 Let M ⊧ CET^{∗} and ξ be a finite type covering. Then for all d ∈| M | there is a t ∈ ξ and a variable assignment V s.t. d = t^{M,V}.

From the latter we can prove the following:

Corollary F.3 (Soundness of CASE) Let P be definite and ϕ[\overline{x_{n}}] a wff in the same language. Let \overline{ξ_{n}} be a finite covering of \overline{t_{n}}. Then P ∪ CET^{∗} ⊧ ∀ϕ[\overline{t_{n}}] if P ∪ CET^{∗} ⊧ ∀ϕ[t_{j_{i}}^{i}] for all t_{j_{i}}^{i} ∈ ξ_{i}.

This justifies the CASE inference rule: by using DCA, a finite covering for a term t is representative of all instances of t. Hence proving a statement for a finite exhaustive set is enough for introducing the universal.

Finally, we formulate this CASE rule.

Definition F.4 Let ϕ[\overline{x_{n}}] with free variables x_{i} : τ_{i} and for i ∈ [1..n] let {t_{1}^{i}, …, t_{m_{i}}^{i}} be a covering for t_{i} of the appropriate types: then

\frac{∀ϕ[\overline{t_{m}^{1}}] ⋯ ∀ϕ[\overline{t_{m_{n}}^{n}}]}{∀ϕ[\overline{t_{n}}]} t_{1}^{i}, …, t_{m_{i}}^{i}/t_{i}

Lemma F.2 allows us to use the following simplified format of the CASE rule:

Definition F.5 Let ϕ[\overline{x_{n}}] with free variables x_{i} : τ_{i} and for i ∈ [1..n] let {t_{1}^{i}, …, t_{m_{i}}^{i}} be a covering for x_{i} of the appropriate types: then

\frac{∀ϕ[\overline{t_{m}^{1}}] ⋯ ∀ϕ[\overline{t_{m_{n}}^{n}}]}{∀ϕ[\overline{x_{n}}]} t_{1}^{i}, …, t_{m_{i}}^{i}/x_{i}

We will denote with CASE^{−} the version of the rule restricted to goals (literals, for the time being).

Then we can state a completeness result for CASE: indeed the only logical atomic consequences of the form ∀p(\overline{t_{n}}) of P ∪ CET^{∗} induced by the DCA are those provable by case analysis.

Proposition F.2 Let P be definite and p(\overline{t_{n}}) a possibly open atom. Let \overline{ξ_{n}} be a finite covering of \overline{t_{n}}. Then P ∪ CET^{∗} ⊧ ∀p(\overline{t_{n}}) iff P ∪ CET^{∗} ⊧ ∀p(\overline{t_{n}}^{i}) for each \overline{t_{n}}^{i} from the covering \overline{ξ_{n}}.

Finally we sum up the relationship among P, comp(P), CET and CET^{∗}. It should come as no surprise that:

• P ∪ CET and P ∪ CET^{∗} are equivalent modulo positive ground atoms

• comp(P) ∪ CET and comp(P) ∪ CET^{∗} are equivalent modulo negative ground atoms and universal negative queries

• P ∪CET^{∗} is a conservative extension of P ∪CET modulo positive universal queries.

We conclude this section with the following lifting property:

Proposition F.3 Let P be definite and p(\overline{t_{n}}) a possibly open atom. Let \overline{ξ_{n}} be a finite covering of \overline{t_{n}}. Then if p(\overline{t_{n}}^{i}) from the covering fails finitely, so does p(\overline{t_{n}}).

The converse of this proposition is painstakingly proven in the appendix of [90].

F.3 CASE-Elimination

While the model-theoretic results of the previous section may be satisfying for the Horn setting, they are not straightforwardly generalizable to the more expressive framework we are interested in. We thus turn to proof-theory and show what we may call, with a jazzy term, CASE-elimination.

This actually boils down to showing that the rule of proof by case analysis is admissible w.r.t. systems augmented with the DCA. Indeed, the latter is derivable from the former in minimal logic with predicate congruence. Roughly, we can eliminate a CASE step by a sequence of applications of the DCA corresponding to the “depth“ of the covering, which is formalized in Definition F.3 by the notion of case-rank. This is then iterated on the whole derivation as usual. The base case is given by Lemma F.3. We need some additional terminology.

Definition F.6 We say that a covering ξ is relevant to ϕ_{L_{Σ}} if

• ϕ is a formula in the language L_{Σ} of the form ∀x : τ.ψ for a type τ ∈ T ype

• ξ is a τ-covering.

We use the notation CASE_{ξ}^{ϕ} for an application of CASE to a formula ϕ according to a relevant covering ξ. In particular CASE_{δ(τ)}^{ϕ} is the canonical rule, i.e. it uses the canonical covering δ(τ). Finally, let Cng(ϕ) be the congruence axioms for the predicate symbols occurring in ϕ_{L_{Σ}} ^{30}. We will shorten the notation when it does not lead to ambiguity.

Lemma F.3 For a given ϕ in L_{Σ}: DCA, Cng(ϕ) ⊢_{M} CASE_{δ(τ)}^{ϕ}.

Proof. A simple derivation in minimal logic. □

Trivially this holds for CASE_{δ(τ)}^{−}.

Lemma F.4 (Admissibility of CASE) Let ξ = t_{1}, …, t_{n}/x : τ be a relevant covering for ∀x : τ.ϕ ∈ L_{Σ}. For i ∈ [1, n], let D_{i} :: ∀_{τ} [t_{i}/x]ϕ be a CASE-free derivation in minimal logic with DCA and Cng(ϕ) Then there is a case-free derivation E :: ∀x : τ.ϕ in the same system.

Proof. By induction on the case-rank.

• Let cr(ξ) = 0. Then ξ = δ(τ) and the result follows from Lemma F.3.

• Let cr(ξ) = n + 1. By inductive hypothesis.

□

Corollary F.4 (CASE-Elimination) P, CASE ⊢_{M} ϕ entails P, DCA, Cng(ϕ) ⊢_{M} ϕ

Proof. By structural induction of the derivation. For each inference rule which is not CASE, we appeal to the inductive hypothesis applied to the premise(s). Otherwise it is a CASE_{ξ} with cr(ξ) = n: apply IH to the premises and admissibility of CASE to recover the cut-free derivations. □

The converse of Lemma F.3 does not hold for the literal version of CASE:

Lemma F.5 For a given ϕ in L CASE_{δ(τ)}^{ϕ}, Cng(ϕ) ⊢_{M} DCA

Proof. For the sake of simplicity consider the case of the signature of numerals: then let ϕ[0] be 0 = 0 ∨ ∃y.0 = s(y) and ϕ[s(x)] be ∀x.s(x) = 0 ∨ ∃y.s(x) = s(y) and conclude by CASE. □

Corollary F.5 (Equivalence) P, CASE ⊢_{M} ϕ iff P, DCA, Cng(ϕ) ⊢_{M} ϕ

F.3.1 Refinements: More on DCA

This part is skipped; it contains a different formalism which will be fixed soon.

30In the higher-order setting predicate symbols belong to the signature and Cng(ϕ) is just the Cng axiom in CET, but we opt to keep it separate. In fact at first-order they are not related to the signature and thus do not concern the free equality theory; second we know that its weak versios are derivable from the completion and finally we prefer not to assume calculi with built-in equality.

F.3.2 CASE and Induction

Of course, proof by case analysis must not be confused with induction, as it is, after all, only a limp, stepless induction.

Example 13

\begin{matrix}p(0) \\ Πx.p(s(x)) ← p(x) \end{matrix}

the query ← ∀x.p(x) fails, since an inductive step is required, although the query ← p(N) succeeds for every numeral n. ◇

Actually it is an easy consequence of the CASE/DCA equivalence that in certain theories, the addition of CASE, either as an axiom or a rule, is immaterial w.r.t. provability. Let P A − IND be the Peano axioms minus induction.

Corollary F.6 T h(P A − IND ∪ CASE) = T h(P A − IND).

Proof. DCA_{NAT} is provably equivalent to the third Peano axiom as in Enderton’s textbook axiomatization. □

Since the latter axiom ensures that every element in the domain of the model can be construed (even not effectively) out of the signature of the relevant axioms, this suggests the following generalization:

Conjecture F.1 Let K be the class of reachable models: if A is a set of axioms which hold in M ∈ K, then T h(A ∪ CASE) = T h(A).

Yet, it may be thought that there is some connection with the ω-rule in arithmetic and its usage for cut-elimination. After all, the latter coincides with the CASE rule with an infinite domain covering. Well, it can be shown that the results in [12] do not hold for infinite coverings. Indeed Proposition F.1 and therefore Corollary F.3 are falsified, e.g. by considering an infinite nat-covering: clearly it does not cover any domain of a model of CET^{∗} not isomorphic to the numerals. This is the case for Proposition F.3, too.

F.4 The CASE algorithm

The problem is now to integrate CASE with SLD. Actually it seems we have made no progress, since we have substituted an extensional universal with more extensional universals. Yet Lemma F.1 roughly suggests this is not a regressio ad infinitum.

The proposal in [12] is to use an ad hoc algorithm to solve universal queries stemming by inversion on the CASE rule. This is actually achieved for Σ2formulae.

Definition F.7 [Correct answer for Σ2-formulae] Let ϕ(x : τ, y : τ′) be a quantifiers free formula—usually a Horn goal—and θ_{1}, …, θ_{n} correct answers for ∃y∃xϕ s.t. for all i ∈ [1..n]

1. θ_{i}(x) is a τ-covering

2. There is θ s.t. θ = mgu(θ_{i}(y)).

Then θ(y) is a correct answer for ∃y∀xϕ.

The idea is thus to produce a possibly infinite sequence of correct answers from the existential goals looking for a subsequence that satisfies the above conditions. The bindings for the universal variable are regarded as partial type-covering: the algorithm stops when the type is covered and there exists an mgu for the existential one. The state on which we compute is a set of triples ⟨θ, U, L⟩, where θ is the candidate mgu, U records what it is still to be covered and L contains the initial sequence of substitution. Rather then giving more details, we trace the computation on the nonpath example 9 using LP AP rolog^{@}. Note that the program in the paper is wrong: the third

clause is not nonpath(X,Y,[Z|ZS]):-nonpath(X,Y,ZS). Moreover, the clause
nonedge(b,a) is subsumed by nonedge(E,a).
nonpath(X,Y,[]):-nonedge(X,Y).
nonpath(X,Y,[Z|ZS]):-nonedge(X,Z).
nonpath(X,Y,[Z|ZS]):-nonpath(Z,Y,ZS).
/* nonedge(b,a). */
nonedge(b,b).
nonedge(c,Z).
nonedge(Z,a).
nonedge(a,c).

Consider the query ← ∃Y ∀Xs : nonpath(c, Y, Xs) which succeeds with computed answer Y = a, as the values for X given by θ_{1}, θ_{2}, θ_{3} are a covering for list(el).

Note that the algorithm does not automatically backtrack and cannot find the other answers Y = b, Y = c. Again operationally it might be though that this is due to the impossibility of finding suitable mgus for Y. Actually, this could be fixed with a simple restart mechanism which would reinitialize θ to ϵ and U to τ.

It seems that there is something inherently fishy in the inter-relationship between the CASE algorithm in [12] and SLD.

F.5 Extensional Uniform Proofs

We formulate a system of uniform proofs with extensional quantifiers so that the result is still an abstract logic programming language which extends conservatively the given one—in this case the implication free fragment of hhf. We do this in two steps. First we describe a very high level non deterministic system that we then refine to an actual interpreter (in a continuation-passing style).

Consider Horn clauses and its extension UPiHorn with the two universal quantifiers:

D ::= A|G ⊃ D|D_{1} ∧ D_{2}|ΠxD
G ::= A|G_{1} ∧ G_{2}|G_{1} ∨ G_{2}|∃xG|∀xG|ΠxG

Recall the operational semantics of uniform proofs for this fragment:

P ⊢ G_{1} ∧ G_{2} iff P ⊢ G_{1} and P ⊢ G_{2}  AND
P ⊢ G_{1} ∨ G_{2} iff P ⊢ G_{1} or P ⊢ G_{2}  OR
P ⊢ ∃xG iff there is a closed term t s.t. P ⊢ [t/x]G INST ANCE
P ⊢ ΠxG iff P ⊢ [a/x]G for a eigenvariable ’a’  GENERIC

To those search operations we add:

P ⊢ ∀x : τ.G iff P ⊢ Π[t_{i}/x].G for t_{1} … t_{n}/x CASE

Call this extensional uniform proofs (⊢_{eu}). The idea is to ‘guess‘ the correct covering for x : τ and them proceed with the intensional interpretation. As a matter of fact, we are factoring out the guessing game, much in the same style the INSTANCE operation is treated. In the high-level version, the right term is guessed and substituted. This is later operationally refined by using unification to provide the instantiation.

Example 14 Let Γ be the following program:

ΠX.r(X) ← p(X).
ΠX.r(X) ← q(X).
p(0).
p(s(0)).
ΠX.q(s(s(X))).

We trace the evaluation of query Γ ⊢_{eu} ∀X.r(X)

Γ ⊢_{eu} q(ssa)
Γ ⊢_{eu} p(0)  Γ ⊢_{eu} p(s0)  \overline{Γ ⊢_{eu} r(ssa)}
\underline{\overline{Γ ⊢_{eu} r(0)}}  \overline{Γ ⊢_{eu} r(s0)}  \underline{\overline{Γ ⊢_{eu} Πy.r(ssy)}}
\overline{Γ ⊢_{eu} ∀X.r(X)}^{case}
◇

From Corollary F.5 we get

Corollary F.7 P, CASE ⊢_{M} ∀x.G iff P, DCA, Cng(G) ⊢_{M} Πx.G

Claim F.1 P ⊢_{eu} G iff P, CET_{c}^{∗} ⊢_{M} G

To be completed

F.6 An Interpreter

We assume two sets of parameters, the usual ones a, b, c and the splittable ones \overline{a}, \overline{b}, \overline{c} etc.... Those are the ones introduced by Π immediately after a CASE application (in a bottom-up search). The technique could be called a form of iterative deepening search, since, upon reports of clashes among splittable parameters and clauses, deeper coverings have to be tried. It would seem plausible to push the choice of the covering, i.e. the instantiation of the splittable parameter, to the atomic level and inserting there the backtracking point, thus avoiding a premature commitment. This would mean adding the following clause to the immediate implication final condition something like:

\frac{P ⊢ A >> [t_{i}/x]A}{P ⊢ A >> [\overline{a}/x]A}t_{1} … t_{n}/x

Yet this is at once incomplete as it is shown by the previous example.

Example 15 r(X) :- p(X).
r(X) :- q(X).
p(0).
p(s(0)).
q(s(s(X)).

Given the query ∀X.r(X) we need to split immediately at the root rather than propagating the parameter thru backchaining on the first clauses. Note that two splitting have to be tried. Upon failure, control must be given back to the initial query, that will submit the correct covering.

Some Elf high level code for the interpreter^{31}:

31to be inserted

G HO-q

How do we lift those results to higher-order logic? One possibility not pursued here is to reduce higher-order problems to FO-problems modulo the ηβ equality theory, as in [25], possibly using what Kirchner calls Syntactic theories.

The other it to formulate axioms for higher-order finite tress (E_{ΣT ω}). Given the undecidability results, we cannot expect something like 1. What we can do is start with patterns. Assume a suitable notion of substitution.

Definition G.1 [patterns]

Notation G.1 higher-order terms are assumed to be in long βη normal form and normalization is performed after every rewrite step. For the sake of readability, variables stand for their normal form, for example Z : i → o stands for λx : i.Z(x).

We tacitly assume for the moment that (dis)equations are well- typed. On the other hand we parametrize Dca to kind declaration, i.e. for each context containing say τ : type we have a Dca(τ)

Definition G.2 [Freeness theory for patterns]

• Equality axioms for λ-terms

\begin{matrix}(β) : & (λx.M)N = [N/x]M \\ (η) : & λxMx = M \\ () : & M = N → λx.M = λx.N \\ () : & N = N′ → MN = MN′ \\ () : & M = M′ → MN = M′N \\ (Ref) : & M = M \\ (Sym) : & M = N → N = M \\ (T rs) : & M = N ∧ N = P → M = P \end{matrix}

• Finite trees axioms

(Dec) :  λ\overline{x_{k}}.a(∼) ≠ λ\overline{x_{k}}.a(\overline{t_{n}}) → \overline{λ\overline{x_{k}}.s_{n} = λ\overline{x_{k}}.t_{n}} a ∈ Σ ∪ \{\overline{x_{k}}\}
(Clh) :  λ\overline{x_{k}}.a(∼) ≠ λ\overline{x_{k}}.a(\overline{t_{m}})  a ≢ b, a, b ∈ Σ ∪ \{\overline{x_{k}}\}
(Oc1) :  λ\overline{x_{k}}.F (\overline{y_{m}}) ≠ λ\overline{x_{k}}.a(∼)  F ∈ F V (∼)
(Oc2) :  λ\overline{x_{k}}.F (\overline{y_{m}}) ≠ λ\overline{x_{k}}.a(∼)  a ∈ F V (\overline{x_{k}}) − F V (\overline{y_{m}})
(Dca(τ)) : ∀X( ⋁_{f^{\overline{τ}→τ} ∈Σ} ∃\overline{Y} (X = f(\overline{Y})))

Oc1 is called a cycle and properly corresponds to Ock; Oc2 is instead called a bound variable capture or more simply a capture and it is peculiar to the higher-order order nature of the term algebra: it happens in the case a would get bound in the substitution.

Example 16 Given Σ = {all : (i → o) → o, imp : o → o → o, and : o → o → o} for kinds i, o : type, Dca(o) is

∀X : o (∃C : i → o.X = all C ∨ .∃P_{1}, P_{2} : o.x = imp P_{1} P_{2} ∨ x = and P_{1} P_{2})

◇

Note that to allow the generality present in first-order disunification we should provide an algebraic model for higher-order terms: we limit only to the higher-order Herbrand universe.

Lemma G.1 (Clark lemma for higher-order patterns) Let s and t be two patterns:

1. if they are unifiable, E_{ΣT ω} ⊢ ∃(s = t)

2. if not E_{ΣT ω} ⊢ ∀(s ≠ t)

Theorem 5 E_{ΣT ω} is decidable

REFERENCES 43

References

[1] Aczel A. An Introduction to Inductive Definitions. In Handbook of Mathematical Logic, Barwise J. (ed.), North-Holland, 1977.

[2] S. Akama. On the Proof Method for Constructive Falsity. ZML 34, 385–392, 1988.

[3] Apt K.A. & Van Emden M.H. Contributions to the Theory of Logic Programming. JACM, vol. 29, no. 3, pp. 841-862, 1982.

[4] Apt K.A., Blair H. A. & Walker A. Towards a Theory of Declarative Knowledge. In: Foundations of Deductive Databases and Logic Programming, Minker J. (ed.), pp. 89-148, Morgan Kaufmann, 1988.

[5] Apt K.A. Logic Programming, Handbook of Theoretical Computer Science, Leuween J. (ed.), Elsevier, 1990.

[6] Apt K.A. & Bol R. Logic Programming and Negation: A Survey. Journal of Logic Programming, To appear.

[7] Aronson M. , Eriksson L-H. , Hallnss L. & Kreuger P. A Survey of GCLA: a Definitional Approach to Logic Programming. In: Extensions of Logic Programming, Schroeder-Heister P. (ed), LNAI, vol. 475, Springer-Verlag, 1991.

[8] Barbuti R., Mancarella P., Pedreschi D. & Turini F. Intensional Negation of Logic Programs. Tapsoft87, LNCS vol. 259, Springer Verlag , pp. 96–110,1987.

[9] Barbuti R., Mancarella P., Pedreschi D. & Turini F. A Transformational Approach to Negation in Logic Programming. Journal of Logic Programming, 8(3), pp. 201-228, 1990.

[10] Bonner A. J. & McCarthy L. T. Adding NF to Intuitionistic Logic Programmninhg. Proc. North American Conf. on Logic Programming, pp. 681– 73, MIT Press 1990.

[11] Brezau-Tannen V. Combining Algebra and higher-order types. In Proceedings of the IEEE Symposium on Logic in Computer Science, 1988, pp. 82–90, 1988.

[12] A. Brogi, P. Mancarella, D. Pedreschi & F. Turini. Universal Quantification by Case Analysis.ECAI-90, pp. 111–116, 1990.

[13] F. Bruscoli, F. Levi, G. Levi and M.C. Meo. Intensional Negation in Constraint Logic Programming. Proceedings of GULP93, D. Sacca’, ed., pp. 359–373, 1993.

[14] Búrchert H.J. Solving Disequations in Equational Theories. CADE88, LCNS 310, pp. 517–526, Spriger Verlag.

[15] D. Chan. Constructive Negation Based on the Completed Database. In Proceedings of the Fifth International Conference and Symposium on Logic Programming, R. Kowalski and K. Bowen, eds., pp. 111–125, MIT Press, 1988.

[16] D. Chan. An Extension of Constructive Negation and its Application in Coroutining. In Proceedings of North American Conference on Logic Programming, E. Lusk and R. Overbeek, eds., pp. 477–493, MIT Press,1989.

[17] Clark K.L. Negation as Failure. In: Logic and Data Bases, Gallaire H. & Minker J. (eds.), Plenum Press, New York, pp. 293-322, 1978.

[18] A. Colmerauer. Equations and Disequations on finite and infinite trees. FGCS84, pp.85–99, 1984.

[19] Comon H. Unification et Disunification: Theorie et Applications. Thesis de Doctorat, I.N.P. de Grenoble, 1988.

[20] Comon H. & Lescanne P. Equational Problems and Disunification. Journal of Symbolic Computation, 7, 371–425.

[21] Comon H. Disunification: A Survey. In: Computational Logic, Lassez & Plotkin (eds.), MIT Press 1991.

[22] Comon H. Elimination of Negation in Equational Theories. Technical Report, Paris-Sud, 1993.

[23] Constable R. et al. Implementing Mathematics with the Nuprl Development System. Prentice-Hall, 1986.

[24] Dart P.W. & Zobel J. A Regular Type Language for Logic Programs. In Types in Logic Programming, Pfenning F. (ed.), pp. 157-187, MIT Press, 1992.

[25] Dowek G. , Hardin T. & Kirchner C. Higher-Order Unification via Explicit Substitution. ?

[26] Dougherty D.J. Higher-Order Unification via Combinators. Theoretical Computer Science, 113:273–298, 1993.

[27] . Drabent, W. What is Failure ? An Approach to Constructive Negation. Acta Informatica, 32, pp. 27–59, Springer Verlag, 1995.

[28] L. -H. Erikkson. Finitary Partial Definition and General Logic. Extensions of Logic Programming, Schroeder-Heister P. (ed), LNAI, vol. 475, Springer-Verlag, 1991.

[29] L. -H. Erikkson. Finitary Partial Definition and General Logic. Ph.D. thesis, Royal Institute of Technology, Stockholm, 1993.

[30] Felty A. Encoding Dependent Types in an Intuitionistic Logic. In: Logical Frameworks, Huet & Plotkin (eds.), Cambridge University Press, pp. 215-251, 1991.

[31] Foo N, Rao A., Taylor A. & Walker A. Deduced Relevant Types and Constructive Negation. Proc. 5th Conf. Logic Programming, Kowalski B. & Bowen K. (eds.), pp.126-139, 1988.

[32] Gabbay D. M. Modal Provability Interpretations of NF. In: Extensions of Logic Programming, Schroeder-Heister P. (ed), LNAI, vol. 475, Springler-Verlag, 1991.

[33] Gabbay D. M. & Reyle U. N-Prolog: an Extension of Prolog with Hypothetical Implications: 1. Journal of Logic Programming, 4, pp. 319-355, 1984

[34] Gabbay D. & Sergot M. Negations as Inconsistency: I. Journal of Logic Programming, pp. 1-36, 1986.

[35] Gecseg F. & Steinby M. Tree Automata. Akademiai Kiado, Budapest, 1984.

[36] M. Gelfond & V. Lifschitz. Logic Programming with Classical Negation. In: Proc ICLP90, MIT Press, 1990.

[37] Ginsberg M L. Negative Subgoals with Free Variables, Journal of Logic Programming,11, pp. 271-293, 1991.

[38] Giordano L. & Olivetti N. NF in Intuitionistic Logic Programming. In Apt K. (Ed.), JCSLP92, pp. 431–445, MIT Press 1992.

[39] J-H. Girard Y. Lafont & P. Taylor. Proof and Types, Cambridge University Press, 1991.

[40] J. Gougen & J.J. Horning. The Algebraic Specification of Abstract Data Types. Acta Informatica,10:27–55,1978.

[41] Y. Gurevich, Intutionistic Logic with Strong Negation. Studia Logica36, pp. 49–59, 1977.

[42] Jacobs B. & Melham T. Translating Dependant Type Theory into Higher-Order Logic. In: Typed λ-Calculi and Applications, Bezem & Groote (eds.), pp. 209-229, Springler-Verlag, 1993.

[43] Jaffar J., Lassez J-L. & Lloyd J.W. Completeness of the Negation as Failure Rule. In: IJCAI-83, Karlsurhe, pp. 500-506, 1983.

[44] Jäger G. Between Constructive Mathematics and PROLOG. Arch Math. Logic, 30:297-310, 1991.

[45] Jäger G. Some Proof-Theoretic Aspects of Logic Programming. In: H. Schwichtenberg (ed.) Algebra And Logic of Specification, Springer-Verlag, Berlin 1993.

[46] Johansonn I. Der Minimal Kalkul, ein Reduzierter Intuitionistischer Formalismus, Compositio Mathematica, vol. 4, pp. 119-136, 1936.

[47] Hallnäs L. Partial Inductive Definitions. Theoretical Computer Science, v. 87 no. 1, pp. 115-147, 1991.

[48] L. Hallnäs & P. Schroeder-Heister. A Proof-Theoretic Approach to Logic Programming: Clauses as Rules. Journal of Logic and Computation, v.1 no. 2. pp. 261-283, 1990.

[49] L. Hallnäs & P. Schroeder-Heister. A Proof-Theoretic Approach to Logic Programming: Programs as Definitions. Journal of Logic and Computation, v.1 no. 5. pp. 635-660,1991.

[50] Harland J. On Hereditary Harrop Formulae as a Basis for Logic Programming. PhD Thesis, Edinburgh 1991.

[51] J. Harland. A Clausal Form of the Completion of Logic Programs. In Proceedings of the Eighth International Conference on Logic Programming (ICLP’91), pp. 711 –725, MIT Press, 1991.

[52] Harland J. Towards a Static Proof System for Negation as Failure. Citri/TR-92-49, University of Melburne, 1992.

[53] Harper R., Honsell F. & Plotkin G. A Framework for Defining Logics. JACM, 40(1):143–184, 1993.

[54] Heintze N. & Jaffar J. Semantic Types for Logic Programs. In Types in Logic Programming, Pfenning F. (ed.), pp. 141-156, MIT Press, 1992.

[55] P.M. Hill and J.W. Lloyd. The Gödel Programming Language, MIT Press, 1994.

[56] Kirchner C. & Lescanne P. Solving Disequations. Proceedings of the IEEE Symposium on Logic in Computer Science, 1987, pp. 347–352, 1987.

[57] Kirchner C. & Klay F. Syntactic Theories and Unification. Proceedings of the IEEE Symposium on Logic in Computer Science, 1990, pp. ??–??, 1990.

[58] Kunen K. Negation in Logic Programming. Journal of Logic Programming, 4, pp. 289-308, 1987.

[59] Kunen K. Answer Sets and NF. In: Proceeding of ICLP87, pp. 219-228, MIT Press,1987.

[60] M.R. Krom. THe Decision Problem for a Class of First-Order Formulas in which all Disjunctions are Binary. Zeit. math. Logik, 13,15–20, 1967.

[61] Kuper G.M., McAloon K.W., Palem K.V. & Perry K.J. Efficient Parallel Algorithms for Anti-Unification and Relative Complement. Proceedings of the IEEE Symposium on Logic in Computer Science, 1988, pp. 112–120, 1988.

[62] K. Kunen. Negation in Logic Programming. Journal of Logic Programming, 4, 289– 308, 1987.

[63] Lassez J.-L. & Maher M J. Closure and Fairness in the Semantics of Logic Programming, T CS, 29:167-184 1984.

[64] Lassez J-L. & Marriot K. Explicit Representation of Terms Defined by Counter Examples. Journal of Automated Reasoning, 3, (3), pp. 301-317, 1987.

[65] Lassez J-L., Maher M.J. & Marriot K. Unification Revisited. In: Foundations of Deductive Databases and Logic Programming. Minker J. (ed.), Morgan Kaufmann, pp. 587 -626, 1988.

[66] Lassez J-L., Maher M.J. & Marriot K. Elimination of Negation in Term Algebras. In: Mathematical Foundations of Computer Science. Tarlecki A. (ed.), Springer-Verlag, pp. 1-16, 1991.

[67] Levi F. Constructive Negation and Universal Quantification. M.S. Thesis, Universita’ di Pisa, 1992.

[68] Lloyd J.W. Foundations of Logic Programming. Second Extended Edition, Springer-Verlag, Berlin, 1987.

[69] Lloyd J.W. & Topor R.W. Making Prolog more Expressive. Journal of Logic Programming, 1, 3, pp. 225-240,1984.

[70] Lloyd J.W. & Topor R. W. A Basis for Deductive Database Systems I and II. Journal of Logic Programming, 2, 2, pp. 93-109, 3, 1, pp. 56-67, 1986.

[71] Lloyd J.W. & Shepherdson J. Partial Evaluation In Logic Programming, Journal of Logic Programming, v.11, pp. 217-242, 1991.

[72] Loveland D. Near-Horn Prolog and Beyond, Technical Report CS-1988-25, Duke University, 1988.

[73] Lugiez D. Positive and Negative results for Higher-Order Disunfication. Journal of Symbolic Computation, to appear

[74] Maher M. J. Complete Axiomatization of the Algebras of Finite, Rational and Infinite Trees. In: Proceedings of the IEEE Symposium on Logic in Computer Science, 1988, pp. 348–357, 1988.

[75] Mal’cev A.I. Axiomatixable Classes of Locally Free Algebrae. In The Metamathematics of Algebraic Systems: Collected Papers, 1936–1937, pp. 262–289, North-Holland, 1971.

[76] Maluzinski J. & Naslund T. Fail Substitutions for Negation as Failure. Proceedings of NACLP ’89, Lusk & Overbeek (eds.), MIT Press, pp. 461-476, 1989.

[77] Mancarella P. , Martini S. & Pedreschi D. Complete Logic Programs with Domain Closure Axiom. Journal of Logic Programming, 5, pp. 263-276, 1988.

[78] McCarty L. F. Fixed Point Semantics and Tableau Proof Procedures for a Clausal Intuitionistic Logic, Technical Report LRP-TR-18, Rutgers,1986.

[79] Miller D. A Logical Analysis of Modules in Logic Programming. Journal of Logic Programming, pp. 79-108, 1989.

[80] Miller D. A Logical Programming Language with Lambda-Abstraction, Function Variables and Simple Unification. In: Schroder-Heister P. (ed.) Extensions of Logic Programming, LNAI 475, Springer-Verlag, pp. 253–281, 1991.

[81] Miller D., Nadathur G., Pfenning F., Scedrov A. Uniform Proofs as a Foundation for Logic Programming. Annals of Pure and Applied Logic, 51, pp. 125-157, 1991.

[82] D. Miller. FORUM etc... LICS93

[83] Minker J. On Indefinite Data Bases and the Closed World Assumption. Proc. 6th Conf. Automated Deduction, LNCS 138, Springer-Verlag, Berlin, 1982.

[84] Minker J., Rajasekar A. & Lobo J. A Theory of Disjunctive Logic Programs, in: Computational Logic, Lassez J.L. & Plotkin G. (eds.), MIT Press, 1991.

[85] Mishra P. Towards a Theory of Types in Prolog. In: Proc. of the 1984 Symposium on Logic Programming, pp. 289–298, 1984.

[86] Momigliano A. Prolog and Negation, M. S. Thesis, Computing Laboratory, Department of Mathematics, Oxford University, 1989.

[87] Momigliano A. Hereditary Harrop Formulae and Minimal Negation, in: Logic Foundations of Computer Science, Nerode A. (ed.) LNCS no. 676, Springler-Verlag, 1992.

[88] Momigliano A. Some Remarks on Uniform Proofs and Constructive Negation , M. S. Thesis, Department of Philosophy, Carnegie Mellon University, 1993.

[89] Momigliano A. & Ornaghi M. Regular Search Spaces as a Foundation of Logic Programming. In: Extensions of Logic Programming, Dyckhoff R. (ed.), LNAI no. 425, Springler-Verlag, 1994.

[90] Momigliano A. & Ornaghi M. Regular Search Spaces and Constructive Negation. Journal of Logic and Computation, to appear.

[91] Moreno Navarro J.J. Default Rules: An Extension of Constructive Negation for Narrowing-Based Languages, ICLP94, MIT Press, 1994.

[92] Murthy C. Classical Logic as a Programming Language: Typing Nonlocal Control, submitted, 1993.

[93] Nadathur G. A Proof Procedure for the Logic of Hereditary Harrop Formulas, Journal of Automated Reasoning, 11, pp. 115-145, 1993.

[94] Naish L. Negation and Control in Prolog. LNCS no. 239, Springer-Verlag, 1985.

[95] Olivetti N. & Terracini L. N-Prolog and the Equivalence of Logic Program. I. Logic Language and Information, pp. 253-339, 1992.

[96] D. Pearce & G. Wagner. Logic Programming with Strong Negation. In: Extensions of Logic Programming, P. Schroeder-Heister (ed.) Springer LNAI 475, pp. 311-26, 1990.

[97] Pfenning F. & Elliot C. Higher-Order Abstrct Syntax, in: Proc. of SIGPLAN’88, ACM Press, pp. 537-551, 1988.

[98] Pfenning F. Logic Programming in the LF Logical Framework, in: Logical Frameworks, Huet & Plotkin (eds.) pp. 149-182, Cambridge University Press 1991.

[99] Pfenning F. Unification and Anti-Unification in the Calculus of Constructions. Proceedings of the IEEE Symposium on Logic in Computer Science, 1991, pp. 74-85, 1991.

[100] Pfenning F. & Rohwedder E. Implementing the Metatheory of Deductive Systems. In CADE-11, Kapur (ed.), LNAI, Springer-Verlag, pp. 537-551, 1992.

[101] Pfenning F (ed.). Types In Logic Programming, MIT Press, 1992.

[102] Pfenning F. Refinement Types for Logical Frameworks. In: Geuvers H. (ed.) Informal Proceedings of the 1993 Workshop on Types for Proofs and Programs, University of Nijmegen, pp. 285–299, 1993.

[103] Pfenning F. Computation and Deduction, Manuscript 199?.

[104] Plaisted D.A. Non Horn Logic Programming without Contrapositives. Journal of Automated Reasoning, 4, pp. 287-325, 1988.

[105] H. Rasiowa. An Algebraic Approach to Non-Classical Logics. North-Holland, Amsterdam, 1974.

[106] Reed D. W. & Loveland W.D. A Comparison of three Prolog Extensions. Journal of Logic Programming, 12, pp. 25-50, 1992.

[107] Reiter R. On Closed World Data Bases. In Logic and Data Bases, Gallaire & Minker (eds.), Plenum Press, New York, 1978.

[108] Robinson J. A. A Machine-Oriented Logic Based on the Resolution Principle. JACM, 12, (1), pp. 23-41, 1965.

[109] D. Shalin, T. Franzen & S. Haradi. An Intuitionistic Predicate Logic Theorem Prover. Journal of Logic and Computation, pp. 619–656, 2, 1992.

[110] Sato T. & Tamaki H. Transformational Logic Program Synthesis. Proc. Int. Conf. on Fifth Generation Computer Systems, 1984.

[111] P. Schroeder-Heister. Rules of Definitional Reflection. In: Proceedings of the IEEE Symposium on Logic in Computer Science, pp. 222–232, 1993.

[112] P. Schroeder-Heister. Definitional Reflection and the Completion. In: Extensions of Logic Programming, Dyckhoff R. (ed.), pp. 333–347, LNAI no. 425, Springler-Verlag, 1994.

[113] Schwichtenberg H. Proofs as Programs. In: Proof Theory. A Selection of Papers from the Leeds Proof Theory Program 1990, S. Wainer (Ed.), Cambridge University Press 1992.

[114] Shepherdson J.C. Negation as Failure. (II) Journal of Logic Programming, 3, pp.185-202, 1985.

[115] Shepherdson J.C. Negation in Logic Programming. In: Foundations of Deductive Databases and Logic Programming, Minker J. (ed.), Morgan Kaufmann, 1988.

[116] Shepherdson J.C. A Sound and Complete Semantics for a Version of NF. TCS, 65(3): 343-371, 1989

[117] W. Snyder & J.H. Gallier. Higher-Order Unification Revisited: Complete Sets of Transformations. Journal of Symbolic Computation, 8:101-140, 1989.

[118] W. Snyder. A Proof Theory for General Unification. Birkhauser, Boston 1991.

[119] Stärk R. The Proof-Theory of Logic Programs with Negation. PhD. Thesis, University of Bern, 1992.

[120] Stärk R. Cut-Property and Negation as Failure, Technical Report, University of Bern, 1992.

[121] Stärk R. From Logic Programs to Inductive Definitions. Technical Report, University of München, 199e.

[122] Stickel M. A Prolog Technology Theorem Prover: a New Exposition and Implementation in Prolog. 464 SRI International, Technical Note, 46, 4. Menlo Park, California, 1989.

[123] Stuckey P. Constructive Negation for Constraint Logic Programming, Proceedings of the IEEE Symposium on Logic in Computer Science, pp. 328-339, 1991.

[124] Tamaki H. & Sato T. Unfold/Fold Transormation of Logic Programs. Proc. ICLP84, pp. 127-138, 1984.

[125] Tarnlund S. A. Horn Clause Computability. BIT, 17, 2 pp. 215-226, 1977.

[126] J.J. Thiel. Stop Losing Sleep over Incomplete Specifications. Proc. of 11th POPL, 1984.

[127] Troesltra A.S. & van Dalen D. Constructivism in Mathematics, vol 1-2. North-Holland, Amsterdam, 1988.

[128] Van Emden M.H. & Kowalski R.A. The Semantic of Predicate Logic as a Programming Language. JACM, vol. 23, no. 4, pp. 733-742, 1976.

[129] G. Wagner. A Database Needs two kinds of Negation. In: Proc. of Mathematical Fundamentals of Database and Knowledge Systems, Springer, LNCS 495, pp. 357–371, 1991.

[130] G. Wagner. Logic Programming with Strong Negation and Inexact Predicates, JLC, pp. 835-8601,6, 1991.

[131] Wallace M. Negation by Constraints: a Sound and Efficient Implementation of Negation in Deductive Databases. Proc. 1987 Symp. on Logic Programming, Computer Society Press, pp. 253-263, 1987.

[132] H. Wansig. The Logic of Information Structures, Springer LNAI 681, 1991.

[133] Wos L. & McCune W. Automated Theorem Proving and Logic Programming: A Natural Symbiosis. Journal of Logic Programming, pp. 1-53, 1991.

[134] Yardeni E. & Shapiro E. A Type System for Logic Programs. Journal of Logic Programming, 10, pp. 125–153, 1991.