WARNING: THE MATERIAL IN THIS CHAPTER IS AT THIS TIME ONLY A COLLECTION OF OLD STUFF PLUS (SOME) HEADLINES OF TOPICS TO BE COVERED IN THE ACTUAL INTRO AND MUST BE UN-DERSTOOD AS A (PARTIAL) STATEMENT OF PURPOSE. PLEASE SKIP AT FIRST READING

1 Definitions and Notation

We list some relevant notions^{1}. We assume fa,iarity with the following:

• Basic proof theory

• first-order logic programming

• first-order and higher-order unification

We will give the very basic notions of higher-order logic programming

Definition 1.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 1.2 [Contexts] E[F] denotes that the subexpression F inside the brackets has at least one occurrence in E.

Definition 1.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 1.4 [Substitutions]

Definition 1.5 [Ground, Instance, Term Subsumption] Notation 1.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

1under construction

⋀_{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.

For a syntactic object O, F V (O) will denote the set of its free variables.

Definition 1.6 [Simple types] For every type α we assume a set C_{α} of constants and countably infinite set of variables V_{α} such that disjoint …. Put Σ = ⋃_{α∈T} C_{α}

A ::= a | (c a_{1}, …, a_{n}) | A_{1} → A_{2}

Order of types and of Goals

Core language: for the Elf language [?], under the Curry-Howard iso, we can identify universals and implication, the latter being an empty Π.

G ::= P | G_{1} → G_{2} | Πx : A.G
D ::= P ← G
P ::= · | D, P

It can be shown that this equivalent to the following extended language [?, ?]: we will sometimes use the latter for sake of brevity

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

Uniform proofs judgments

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

\begin{matrix}\begin{aligned}G_{1}, P ⊢_{u} G_{2} \\ & S → \\ P ⊢_{u} G_{1} → G_{2} \end{aligned} & \begin{aligned}P ⊢_{u} ∀x.G \\ & S∀^{∗} \\ P ⊢_{u} [a/x]G \end{aligned} \\ \frac{I − atom}{P >> P} & \begin{aligned}P ⊢_{u} D >> P for D in P \\ & S − atom \\ P ⊢_{u} P \end{aligned} \\ \begin{aligned}P ⊢_{u} G \\ & I → \\ P ⊢_{u} (G_{→}P) >> P \end{aligned} & \begin{aligned}P ⊢_{u} ∀x.G >> P \\ & I∀ \\ P ⊢_{u} [t/x]G >> P \end{aligned} \end{matrix}

The rule S∀^{∗} is restricted to the case where the parameter a does not occur in P nor in ∀x.G.

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 [?] and later Shepherdson [] advocated a return to the former approach which makes the treatment of CET nicer. Afterwards Maher [?] set the records straight (to be continued).

2 Classical Negation

It is a basic fact of classical first-order logic that propositional connectives are inter-definable; more precisely some subsets of all operators provides by definition the missing ones; this is an immediate consequence of their truth-value semantics. It is therefore customary and convenient — to save cases in structural inductions — to assume as primitive only some operators and define the others in terms of former with the proviso that they form a complete basis. In almost every definition negation is taken as primitive, paired either with conjunction, disjunction or implication; even those extreme presentations based on a singleton connective as nand or nor retain an implicit flavor of negation. The same remark applies to a notion of negation defined via a propositional constant for falsehood^{2}.

There is yet another way to define negation which is peculiar to classical negation and is related to the transformational approach we are interested in. This is known as negation normal form and it is used for example in Tait’s concise proof of cut-elimination for classical logic ??. For every atomic predicate symbol p we also have a symbol denoting the opposite, say \overline{p}. Then, with the essential usage of double negation elimination and De Morgan s laws, negation is introduced as expected:

2This provably goes back to Kolmogorov and it is motivated by what Girard ?? likes to call the Heyting semantics. We will have more to say in the next chapter.

¬p =_{def} \overline{p}  ¬\overline{p} =_{def} p  ¬¬p =_{def} p
¬(A ∧ B) =_{def} ¬A ∨ ¬B ¬(A ∨ B) =_{def} ¬A ∧ ¬B

Thus, as far as the classical propositional structure is concerned, negation can be achieved by renaming. Consistency is then achieved by adding axioms that specifies that is it inconsistent to hold both p and \overline{p}, i.e. something like p ↔ ¬\overline{p}.

2.1 Renaming to Horn format

For accident or necessity (though now we lean for the former) Horn logic imposed itself as the format in logic programming. Though Turing-complete etc...

A first possibility to be attempted is to investigate how far we can go by renaming to Horn format, especially as negation is concerned.

2.2 Renaming algorithm

Informally, the reasons why this is feasible is classical and intuitionistic logic coincide as far as the Horn format is concerned. Several straightforward prooftheoretical arguments are known ??. This yield that classical equivalences preserve the intended operational semantic of the source program.

2.3 What is failure

Discussion on whether complementation is to be performed only on decision procedures or also on possibly non-terminating programs, r.e. predicates (like demo). What is the failure set of demo?

3 Aim

The aim of this thesis^{3} is to develop a framework for the synthesis of the negation of (logic) programs in logical frameworks such as LambdaProlog, L_{λ} , Lolli, [?, ?, ?] and set the basis for the type-theoretic programming languages Elf, LLF, Twelf [?, ?, ?]. This has an immediate practical relevance in programming in those languages, since it relieves the programmer from the burden of explicitly encoding negative information in the form of type families (higher-order clauses). The main point is to avoid resorting to an operational interpretation of negation-as-failure, NF, whose ultimately troublesome semantics is a serious threat to the implementation, verificationand automatization of the meta-theory of deductive systems . As hinted in the title, the approach that we shall investigate is transformational, started in [?] and developed in [?]. Roughly, given an Elf (hhf) program with occurrences of negated types (predicates), the aim is to derive a new program where the former have been replaced by new positive types (predicates) which correspond to their complement (in a way to be clarified below).

3This section comes from my 1994 proposal and need serious updating

While the topic of negation has been pursued to the extreme in first-order logic programming (we shall try a small review of closely related appraches in ??), the field is almost virgin as far as higher-order logic and type theory is concerned: languages such as λProlog implement NF with the usual cut-fail combination: a logical reconstruction for the first order fragment can be found in Harland’s thesis [?].

Intuitionistic type theories from the simply typed λ-calculus on, say, to Martin-Löf’s Type Theory implement negative types under the Curry-Howard isomorphism as expected, i.e. ¬A ≡ A →⊥, where ⊥ denotes the empty type and DSL is an elimination rule. Thus negative types have no special status, since the emphasis is on functional programs extraction, rather that giving a search (logic programming-like) operational reading to types.

Under the latter interpretation of dependent function types this would correspond to including explicit negative information in the program. Although this is entirely consistent with the procedural interpretation of function types (hypothetical judgments), it has, beyond the aforementioned obvious disadvantage, some additional ones, as we shall argue next.

Though the impetus of this enterprise may seem at first sight mainly pragmatic, it should not be underrated. In short, we are trying to design a reasonable notion of negation, a basic building block of any logic under severe constraints:

“The problem is difficult because it seeks a notion of negation which is simultaneously semantically elegant and computationally feasible: in both execution and mathematical/logical semantics the extended language should cleanly extend the definite clause language” [?].

The reason why NF is so popular in the logic programming (LP) paradigm is that it essentially requires no modification to the search structure of an LP interpreter. Hence most of the effort is to try and show that it also satisfies the other criteria Lassez et al. pointed out. Nonetheless this is just a part of it: quoting from [?]:

“... this notion [NF] is a basic logical notion, a notion of value to pure logic (as studied since the Ancient Greeks) of equal importance and theoretical standing as notion like Possibility, Deduction, Axiom and the like. The role of negation by failure in LP in only a special case: one manifestation of its role in logic”.

Without going overboard, our answer to this plea, will be to show that, paradoxically, the best way to deal with negation in the LP setting (but see ?? for more) is to eliminate it through transformation.

Now, let us see more concretely what it means to us; this reduces to the two intertwined questions: why Elf ^{4}? and why adding negation?

1. Elf: its main edge is the easiness to formalize and verify the metatheory of deductive systems: without mentioning the pedagogical value, Martin-Löf’s idea of judgments-as-types and proof checking as type checking has revolutionized the otherwise painful task of programming proof-checkers. Also the analogy with the difference between the success of logic programming and the unsatisfactory results of general theorem proving may be enlightening. There is perhaps a reasonable middle way between Poincare’s derision to the logicist approach:

“If you need 27 steps to prove that one is a natural number, how many will you need for a real theorem?”.

and Wos’ ambition to have solved with OTTER real mathematical open questions (see [?] for a (distressing) list of them).

2. Negation: Elf is one of the purest, hence poorest in terms of programming language features, systems around; of course this is a conscious design decision to achieve the possibility of expressing, verifying and eventually automating the meta-theory of deductive systems. Indeed, every enlargement of the expressive power of the language has to be carefully crafted, in a declarative way (i.e. without spoiling its inductive character), as in the case of refinement types [?] or otherwise expressed as an outside argument (schema-checking [?]). More explicitly, this amounts to show that every extension is conservative on the operational and declarative semantics of Elf.

An appropriate negation operator may have a rather dramatic effect on the possibility of implementing (i.e. programming) topics that would prove to be too unwieldy to deal with otherwise. Automating the negation of predicates as say typable, well-formed, canonical form etc. will increase the amount of meta-theory that can be checked. Moreover providing negative definitions seems to be particularly error-prone, repetitive and not particularly interesting, thus a good candidate to mechanization. Following this trend a good analogy is the use of higher-order abstract syntax [?]: although it may seem unintuitive at the beginning w.r.t. “named” syntax, it does, notwithstanding the Nuprl group [?], make the difference between being able to master meta-proofs and spending enormous amounts of time in implementing low-level (and tedious) features such as renaming or substitution. To bring this to the extreme, of course, everything can be expressed eventually in first-order logic and ideally proved-checked or even demonstrated by, say, a resolution theorem prover or more likely by an interactive one. In practice, this has turned out to be very problematic, if not a total failure; hence the refinement of the tools to higher-order logic and type-theory. And this is the bottom line: adding another (practically) essential tool to Elf^{5}.

4It may be argued that this is more of relevance to Elf seen as a LP language rather that to LF as a specification metatheory; yet the operational interpretation of LF signatures is independent from the idea of synthesizing negative types

This has an analogy with recent developments in the design of “standard” Prolog-like languages; for external reasons, namely, program transformation, there has been a trend in “logicizing” here at a first-order level built-in predicates such as term comparison, arithmetic, metalogical predicates (see [?]).

Hence the motto seems to be: add features, keep them logical (and constructive).

3.1 Which logical framework

Why we use L_{λ}, if we use it at all. Mention higher-order patterns and the CLP approach to hard higher-order unification problems and lack of quantification over propositions in LF.

4 From Theorem Proving to Prolog and Back

To set the stage^{6} we need to say something on Prolog and how it developed. This enterprise has a rather peculiar parabola Logic programming owes its (relative) success from the way it limits and directs generic theorem proving; from then on, anyway, most of the effort has been to extend its boundaries without falling back onto full clausal logic.

Automatic theorem proving, or at least the intuition (and the dream), can be dated back to Leibniz, but become more of a reality in 1965 when Robinson introduced the resolution principle (for an historical account please refer to [Dav8?] It proceeds by contradiction, converting to clausal form and testing for inconsistency with a version of Gentzen’s cut-rule): Yet, this approach is generally unfeasible given the well-known complexity results. A great deal of research developed after Robinson’s breakthrough aimed at restricting the search space, while preserving completeness.

5Naturally, there is always the problem of enhancing the metalanguage so much that it actually overkills the object level it is trying to specify. Even if the proposed framework is conservative over more manageable systems, we run the risk of having to deal with a overwhelmingly complicated metatheory of the framework for suspicious gains.

6To be reduced sharply; just need to explain why there is no negation in logic programming

This is not the place to give even a short account of these studies: we just sketch those that led to the basis of Prolog as we know it; for references and a chronology see [?].

When building a refutation there are basically two sources of choice:

1. deciding which clauses to pick as parent clauses

2. deciding which literals in those clauses are to be resolved away.

One way to support the first restriction is linear resolution, independently proposed by Loveland and Luckam in 1970.

As far as point 2. is concerned, we may decide, after Hill, Kowalski and Kuehner, to fix the literal to resolve in the center clause (’linear resolution with selection function’)

Though we have narrowed the search space considerably, there is still a fair amount of choice namely conjunctive choince in the side clauses, ancestory tracking and factoring. The winning strategy is to restrict the syntax of the clauses themselves; the choice fell on Horn clauses: definite clauses are interpreted as input ones, while Horn clauses with empty positive part are taken as goals.

Eventually we have arrived at pure Prolog or SLDresolution,

What has SLD-resolution to do with programming? The answer can be found in the so-called procedural interpretation of Horn logic. Although the origins of Prolog are shrouded in mistery, it is known that in 1972 both Kowalski and Colmerauer came up with the idea that (a subset of) logic could be used as a programming language. A definite clause A ← B_{1}, B_{2}, …, B_{n} can be viewed as a definition of an Algol-like procedure:

procedure A
callB_{1}
callB_{2}
⋮
callB_{n}
end

Goal invocation corresponds to procedure invocation, and the ordering of the goals in the body of the invoked clause corresponds to sequencing of statements. In logic programs data manipulation is entirely achieved by means of unification, which encompasses parameter passing, multiple assignment, record allocation, data construction and selection.

In spite of its limits, it can be shown that Horn logic has the same computational power of every usual programming language, i.e. it can (weakly) represent every recursive function [?].

Moreover, Horn logic has some nice model-theoretic properties, namely the minimum model property:

Therefore it has been argued that we should be content with Horn logic, which seems to be a complete and reasonably efficient computational logic. Yet every logician would argue about the impossibility of expressing even the easiest logical problems in a language that lacks (explicit) disjunction and negation; and even from a programming point of view it would not be advisable to have the possibility of performing negative queries and overall to have a negation operator in the body of clauses instead of simulating it with extra- logical constructions, which make programs less understandable and declarative. It is not a question of expressive power, it is a matter of style and convenience.

It is not possible to try to review all the proposed extensions; historically much of the attention has been concentrated on incorporating some form of negation, since from it, most of first-order expressivity is recovered [?].

Negative information is independent from definite (normal) programs.

A specialized inference rule must be invoked: negation as failure (NF), which in logic programming originated from the confluence of two quite different trends of research: the refinements of resolution based automatic proof procedures and the relational a pproach to databases. For a nice introduction see citeShe88. The idea of a proof under the NF rule is a very natural one: suppose you have a set of axioms and some kind of inference mechanism which produces a recursively enumerable set of theorems, and that you are asked to verify the truth of a negative conjecture ¬C under NF; then you try to prove C from your theory; if you succeed, then ¬C does not hold, while if you realize (in a finite time) that C is not provable, then you are entitled to assert that ¬C holds. Its basic idea is to state that a goal is false if we are able to prove that it cannot be proved by the program. Actually NF is more a computational than a logical notion; we answer no to a goal because our attempt to say yes failed, so we say no because we cannot say yes. Differently from other kind of negation, NF ” … does not follow from some constructive knowledge, but from lack of knowledge ” ([?] p. 8). That motivates two specific features of NF: its inability of finding instantiations for the variables of the goals and its non-monotonicity: in fact in real-life databases every enlargement may cause the meaning of failure to change and so turn success into failure.

In logic programming, NF works this way: ” … The basic idea is to use SLD-resolution augmented by NF rule. When a positive literal is selected, we use essentially SLD-derivation to derive a new goal. However, when a ground negative literal is selected, the goal answering process is entered recursively in order to try to establish the negative subgoal … Having selected ground negative literal ¬A in some goal, an attempt is made to construct a finitely failed SLDNF tree with root ← A before continuing with the remainder of the computation. If such a tree is constructed, then the subgoal ¬A succeeds. Otherwise, if a SLDNF -refutation is found for ¬A, then the subgoal fails … ” ([?] p. 87).

5 Extending Horn logic

As previously mentioned, once Horn logic was isolated as the core of a programming language, a fairly disorderly race was off to get more mileage out of PROLOG. This endorsed a failure to consider the two facets of this new style: that not only logic was a powerful programming language, but maybe more importantly that programming can be imbued into logic. While supporters of the first point would go out without lasting results, only the latter, we contend, hit the target.

To elaborate a little, we can isolate several (slightly overlapping) positions:

• The ‘tories’: for model-theoretic reasons, Horn logic is the best possible world , see the manifesto “Why Horn logic matters in computer science” [?]

• The “realists” guided by Apt: logic programming is Horn logic with NF : what’s left to do is logicize the impure features of Prolog

• The “Making Prolog more expressive” people: divided in two main intertwined subtribues: the “logicians”, which claim that programming in Horn logic is like living with a hand tightned behind, and the “compilers” (see Sato and Tamaki. [?]: those come from the specification approach and look at Horn logic as a implementation language which is the target of a long and tiresome travel thru derivation and/or transformations from first-order logic. For the logicians it is a must to conquer any piece of land outside Horn logic, say by adding connectives [?], precompilation [?], change of interpreters (say connection graphs as in Gallier) or switching from classical logic to fragments in the intuitionistic galaxy

• Eventually there is the proof-theoretic approach of uniform proofs: new connectives are allowed only if we can ascribe a clear meaning in term of search and provide a way of endowing logic programming in a purely logical way of features as modules, data abstraction and scoping typical of other mature languages.

5.1 Constructive Negation

Constructive Negation is an attempt to devise methods capable to provide logically justified answers to non-ground negative queries, in analogy with the witnessing property of constructive logics [?]. Formally, for a suitable derivability relation, this property holds when if ⊢ ∃xp(x) then there is a term t s.t. ⊢ p(t) . Accordingly, it is suggested that from ⊢ ∃x¬p(x) the same property infers a term t s.t. ⊢ ¬p(t). We can roughly distinguish two approaches

i. Program Transformation: [?], [?], [?]. ii. Negation by Constraints: [?] for datalog programs, [?] [?] and extended

to CLP in [?]; Fail Substitutions: [?] [?].

Historically, the original attempt to deal with negation was simply to try avoiding the floundering phenomenon: given that the latter is in general undecidable, one possibility is to try to make sure that when a negative literal is called it has already been grounded: there are basically three possibilities:

1. Satisfy the syntactical, though very restrictive, conditions on allowed computations [?], which essentially reduces evaluation to ground evaluation.

2. Try to achieve grounding by delaying as in [M]NU-Prolog or Sicstus, where a goal may be declared to be “frozen” and is evaluated only when it reaches a sufficient degree of instantiation. This is obviously only a partial solution, since at run-time there is no guarantee to eventually ground the problematic query. A further improvement is offered by the computation rules of IC-Prolog (see [?], for a comprehensive analysis and references).

3. Covering the open negative query with a generator of values for the relevant variables.

5.1.1 Static Approaches

If we are dealing with datalog programs, i.e. with finite Herbrand Universe U_{P}, the naive approach would be to instantiate all the rules with potentially troublesome goal with terms from U_{P} [?], say through propagation in every negative literal in the program. This is clearly infeasible, since it may result in an intractable numbers of rules ; besides, this may return many undesired (untypable) answers.

A sophistication of this idea can be found in [?]: the proposal is to automatically infer a ‘type’ for the problematic variables and transform the original program into one where grounding is ensured by coverage from those types. Then useless answers originating from general instantiation would be excluded by the typing discipline. and c is in U_{P}. Although it can be shown that the new program is equivalent to the old one, this cannot be extended to full Prolog: function symbols make the type infinite and non-ground facts would undermine the instantiation capability of the type. What is required is a generator for infinite U_{P}, instead of a table of facts.

The transformational approach has a fairly long history – see [?],for a survey of the early 80’s. The idea is to implement negation using inequalities, so that the negation of any predicate occurring negatively in the original program P is synthesized so as to obtain an equivalent definite program P^{c} (in the sense of F_{P} = M_{P^{c}}). This was first proposed in [?]. In this seminal paper it is shown how to massage the completion so that the derived program mimics failed computation of the original one. The technique consists essentially in taking the contrapositive of the completion, putting the RHS in dnf and eliminating the universal quantified inequalities by introducing a ‘nonunifiable’ predicate. From the simplification of those constraints and by regarding the negated predicate as a new name and through the many-sorted discipline the new definition is obtained.

Two interrelated problems are involved in this simple transformation:

1. We need an explicit way to solve the aforementioned inequalities: this was first suggested in [?] in the general context of explicit representation of generalization and refined in [?]; there it is shown that the uncover algorithm may simplify those constraints into canonical forms but also that this elimination is not achievable in general. Another version, specifically calibrated to the negation issue in its being incremental is given in [?].

2. The presence of local variables, i.e. variables that appear in the body but not in the head is problematic, as they turnout to be universally quantified in an extensional sense.

There have been several partial solution to the above problem: [?] proposes to use a more general fold/unfold transformation system. In [?] instead it is proposed to compute the set-theoretic complement of the terms in the negative predicate compiling away the inequalities.

In the light of the analysis in [?], it is worthwhile to compare the two approaches:

1. Sato/Tamaki:

• locally stratified many-sorted programs

• no local variables

• may be non-left linear

• no explicit mechanism to handle inequalities

• sketch of proof of F_{P} = M_{P^{c}}

2. Barbuti and al.

• left-linear non-stratified programs with no shared local variable in the body, thus reducing the complexity of extensional universal quantification (see below).

• local variables yield non-Horn programs with extensional universal quantification

• left linearization reintroduces inequalities motivating the move to CLP in [?]

• operational interpretation of ∀ 5.1.2 Dynamic Approaches

Chan [?] is acknowledged to be the inventor of the term ’constructive’ negation; his approach can be roughly characterized as a mix of NF with a constraintssolving attitude. In essence it consists in taking a negative goal, calling the positive version and negating the answer obtained. As in the CLP family of languages, unification and disunification are kept explicit and returned as solutions. It is examined in ??. Of course, we need to keep the (in)equalities in normal form and there are some obvious problems when dealing with computations that have infinite answers, addressed in [?], by quantifying over the answer substitutions. No proof of completeness is offered. A generalization to constraint logic programming over arbitrary structures is offered in [?]; it turns out to be sound and complete w.r.t. the three-valued models of the completion. Other development of constructive negation are addressed in [?]^{7}

(E)SLDNF − S ([?]) The finite failure case in the definition of SLDNF - resolution is modified as follows: given the goal ?(Γ, ¬A), then it has a descendent ?θΓ, if there is a finitely failed-tree for ?θA, where dom(θ) ∈ vars(A). So NF instantiates under success, i.e. negative goals directly return substitutions: given P and G the aim is to look for a (fail) substitution θ s. t. P ∪ {θG} has a finitely failed tree; then by the soundness of the NF rule ∀θ¬G is a consequence of comp(P) and thus θ is an a.s. for the query ?¬G. This seems very costly, since it entails enumerating (guessing) every fail substitution.

This is refined in [?], where it is shown how to avoid to generate all possible substitutions in lieu of a maximal general fail substitution. Moreover, the improvement w.r.t. Chan’s work lies in the feature of always including some positive bindings for the variable in the negated goal. If the SLD-tree is infinite, the method enumerates the set of fail substitutions; this corresponds to the fact that in general negative queries cannot be represented by finite positive information alone (connected to [?]).

5.2 Non-Failure Driven Negation

During the years ways of incorporating other more logical forms of negation than NF have appeared. Since most of the time this gives back full non clausallogic, most of them are catalogued as ATP’s. In all these accounts, negative information has to be provided explicitly and specific rules are offered to deal with that. Sometimes it is possible to mix OWA and CWA predicates safely. For a more detailed account and bibliography, let us refer to [?].

• N(Q)Prolog [?] and Negation as Inconsistency ([?]): the former is a complete implementation of positive intuitionistic logic. By defining disjunction classically and allowing a restart rule, Gabbay shows it to be complete for full classical logic as well. The latter evaluates a query against an ordered pair ⟨P, N⟩, where P is a Horn program and N a set of queries that are required not to succeed; this is logically equivalent to adding to the program the negation of all the members of N, and permits importing negative facts and rules. Both systems have a very awkward first-order version.

7check this out

• Stickel’s P T T P, supplementing SLD-resolution with the model elimination rule. This entails keeping track of the ancestors of the goal, loosing one of the key feature of Prolog, namely input resolution. Moreover, due to the directionality of SLD-resolution it requires the inclusion of the contrapositives of the clauses, causing a notable increase in the size of the theory.

• Loveland’s nHP rologincorporating case analysis in SLD-resolution demands each time the invocation of a restart rule, until the stack of unsolved (disjunctive) heads is empty. Without requiring contrapositives it simulates case analysis with different runs of essentially the Prolog engine. Unfortunately naive nH-Prolog is incomplete and the new versions (Progressive nH and Inheritance nH) have a less natural and convincing description.

• Plaisted [?] instead is concerned with a difficult attempt to use sequentbased logic programming with a version of the cut rule which operates backwards leading to a problematic guessing of its premises. For a comparison, see [?].

• Another close relative goes under the name of disjunctive logic programming (see [?] and references therein). It aims to deal with full clausal logic by extending the machinery for Horn Logic.

5.3 Proof-Theoretic Approaches to Negation and NF

Lately we have participated in an attempt to tie LP to proof-theory, where it belongs: and this has brought new insights, particularly on NF.

The first step is to view Horn clauses positively as rules and goals as existentially closed conjunctions of atoms to be proved by the former. Historically this can probably be dated back to Gabbay and Reyle [?]. We can distinguish among two approaches:

1. Clauses as axioms (programs as theories) and some form of Gentzen sequent calculus to infer goals, as it is very clearly expressed in a series of papers by Miller et al. [?]. This approach is also motivated by the enlarged language in consideration (hhf), where every connective and quantifier is allowed by the syntax, though not arbitrarily 2. Clauses as rules [?]: Horn (and beyond) programs should be seen as set of

inference rules for the derivation of (not necessarily ground) atoms. This view is coherent with the idea of programs defining a continuous mapping on the lattice of Herbrand interpretations: then logic programs can be seen as inductive definitions of such interpretations.

This has the following relation with negation:

1. Minimal, intuitionistic and classical negation can be superimposed over Uniform Proofs [?], [?], [?]: Minimal negation, being camouflaged implication, is executed through the AUGMENT/backchain operation ; the evaluation of ¬D consists in the assumption of D and in the attempt to prove ⊥ from the enlarged theory. The Duns Scoto Law and Reductio ad Absurdum for atoms formalize the latter, preserving the feature of abstract logic programming languages [?].

2. GCLA [?] is based on the rule-based definitional approach to LP: it has intuitionistic negation built-in, originating when the definiens operator D returns an empty set of atoms. The calculus D(P) [?] is obtained by adding a definitional rule to C(P) (see ??)

W.r.t. negation-as-failure Stärk [?] has given a sequent calculus NF (P) consisting of

• Clark’s equality and freeness axioms

• Negation (switch) rules

• cut rules, where Σ is a set of equations and Γ of literals.

• Program rules from P, divided into positive and negative introduction.

Much more is however contained in Stärk’s thesis; to quote a few, he shows that a sequent is provable in NF (P) iff it is true in all 3-valued model of the completion. Furthermore a completeness result is proved w.r.t SLDNF - resolution for program satisfying the cut-property [?].

5.4 On substrucural logic and NF

Harland [?] instead proposes a sequent calculus based on intuitionistic logic that directly incorporates NF without referring to the completion. The usual rules, restricted to deal with Horn logic, induce a positive derivability relation; furthermore, he introduces a negative system of disprovability, denoted by ⊢^{−} with judgments of the type: if a conjunction fails then so does one of the conjuncts and so forth. The two systems are interlinked by the rules for NF.

\begin{aligned}Γ ⊢^{−} F \\ & ¬ − R+ \\ Γ ⊢ ¬F \end{aligned}  \begin{aligned}Γ ⊢ F \\ & ¬ − R− \\ Γ ⊢^{−} ¬F \end{aligned}

Structural rules have a paramount importance in this calculus: due to the nonmonotonic nature of NF, weakening in the positive fragment is cautious, introducing only already provable formulae on the left, resulting in a dual to contraction. In the negative system structural rules, cut included, are not eliminable. This is not strictly a calculus of finite failure, since sequents of the form p ← p ⊢^{−} p are provable, although with the essential use of weakening. Of course, due to the recursion-theoretic complexity of unprovability, every such an axiomatic formulation is bound to be incomplete. Moreover the boundary seems fuzzy, as, for example, p is independent from the program p ← q, q ← p. The calculus without structural rules is shown [?] to be sound and complete w.r.t. finite failure and SLDNF -resolution (extended to first-order hereditary Harrop formulae). Still, the system is not meant for proof search and requires a relative complement algorithm to provide answers to open negative queries.

• Cerreto’s linear formalization of NF

• From Bonner, Pareschi: dealing with parsing gaps in Categorial Grammar with NF instead of with linear implication

• Wansig’s strong negation in substructural logics

5.5 My Previous Work

It is maybe worthwhile to review briefly my past work on the subject: [?] is essentially an expository survey of NF from the usual semantic point of view. In [?] and more fully developed in [?] negation in the context of fohh is investigated much (though independently) in the sense of [?]. In [?] a proof-theoretic approach to LP based on the notion of axiom-application rule and regularity is developed. This is refined and applied to constructive negation in [?] through the idea of regular splitting, a manipulation of the completion so as to achieve the same properties of SLD-resolution.

5.6 Contributions and technical acknowledgments

The original contribution of the thesis are:

• a precise casting of first-order and higher-order complement problems as disunification problems

• a complement algorithm for higher-order patterns internalized into a relevant theory of simple types

• a practical treatment of negation for second-order left recursive parametrical judgments

Excusatio non petita: Though the topics addressed are maybe not too deep and somehow not general enough, they required an extensive knowledge and expertise in several fields as negation in logic programming and type theories that are pretty difficult to manage for their sheer size. We contend that our approach is the first one to give a realistic analysis of negation in logical frameworks with an emphasis to the development of a practical tool to incorporate this operator in existing languages.

This work has benefited enormously from the large ensemble of research collected in the Elf and offspring projects: not only form the existence of the Elf language and environment, but also from specific contributions which we have imported (and somehow trivialized) in this thesis. Let me mention only the most recent ones: linear unification (Cervesato and Pfenning), subordination (Virga), mode and termination analysis (Rohwedder and Pfenning), induction schemata and splitting (Schurmann and Pfenning).

Finally I want to point out that Frank Pfenning orginally suggested, among others, the ideas of using relevant types for variables occurences and of augmentation by disequalities.