Elimination of Negation in a Logical Framework

Alberto Momigliano June 20, 2000

Department of Philosophy Carnegie Mellon University Pittsburgh, PA 15213

Submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy

Thesis Committee: Frank Pfenning, Chair Dana Scott Dale Miller

Copyright \begin{matrix}c \\ ◯ \end{matrix} 2000 Alberto Momigliano

Abstract

We address the issue of endowing a logical framework with a logically justified notion of negation. Logical frameworks with a logic programming interpretation such as hereditary Harrop formulae (HHF) cannot express directly negative information, although negation is a useful specification tool. Since negation-as-failure does not fit well in a logical framework, especially one endowed with hypothetical and parametric judgments, we adapt the idea of elimination of negation from Horn logic to a fragment of higher-order HHF.The idea is to replace occurrences of negative predicates with positive ones which are operationally equivalent. This entails two separate phases:

1. Complementing terms, i.e in our case higher-order patterns. Due the issue of dependency constraints, intuitionistic lambda calculi are not closed under complementation. We thus develop a strict lambda calculus, where we can directly express whether a function depends on its argument.

2. Complementing clauses. This can be seen as a negation normal form procedure which is consistent with intuitionistic provability. This entails finding a middle ground between the Closed World Assumption usually associated with negation and the Open World Assumption typical of logical frameworks; the main technical idea is to isolate a set of programs where static and dynamic clauses do not overlap. As this is in general not possible, we isolate a fragment which satisfy this property and has proven to be expressive enough for the practice of logical frameworks.

\underline{ii}

Draft of June 20, 2000

Contents

1 Introduction 3

1.1 Logical Frameworks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.1.1 Negation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.1.2 Which logical framework . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.1.3 What is Failure (in a Logical Framework)? . . . . . . . . . . . . . . . . . . . . . . . . 8

1.2 Negation-as-Failure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.3 From Theorem Proving to Prolog . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.4 Extending Horn Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

1.4.1 Constructive Negation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.4.2 Non-Failure Driven Negation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 1.4.3 Proof-Theoretic Approaches to Negation and NF . . . . . . . . . . . . . . . . . . . . . 13 1.4.4 Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

1.5 Contributions and Technical Acknowledgments . . . . . . . . . . . . . . . . . . . . . . . . . . 14

iv  CONTENTS

List of Figures

Draft of June 20, 2000

2  LIST OF FIGURES

Chapter 1

Introduction

Suppose we are giving a formal definition of a programming language in the style of natural semantics [Kah87]; after we have specified the abstract syntax, the type system (e : τ) and a small step evaluation semantics (e ↦ e′), it is time to check their consistency via a proof of type soundness. We may start by attempting the Progress lemma, which will eventually guarantee that well-typed expressing cannot go wrong; in symbols, this could go like this: for every expressions e such that e : τ and e is not a value, there exists an expression e′ such that e ↦ e′. Now, imagine that our language is fairly sophisticated and our funding agency requires a formal verification of our results. Thus, we decide to use an automated reasoning tool, possibly an interactive one. A proof of progress is a rather trivial structural induction for a human, but in order to be machine checked, it needs to be spelled out in every detail. We may have implemented judgments defining expressions, values, typing and evaluation: but what about the notion of not being a value? We may try to reason in a strictly intuitionistic way and view ¬value(e) as the derivation of a contradiction ⊥ from the assumption value(e). This is possible, but certainly not in the spirit of the proof; ¬value(e) is just a test, a way to sift out expressions that are already fully evaluated. What we really need is a positive (inductive) definition of “not being a value”, say nonvalue(e); indeed, this should be possible, since nonvalues are exactly those expressions which are not values. Nevertheless, manually coding this notion may be tedious and error-prone, especially considering evolution of our initial specification. Moreover, we will also have the obligation of proving, at least to our satisfaction, that the explicit definition of ‘non-value’ coincide with the negation of ‘value’. Lacking this, our formal verification cannot be entirely trusted.

For another example consider a simple instance of reasoning about process algebra, such as Peterson’s algorithm for mutual exclusion [Pet81]. The problem is to ensure that two process can never be simultaneously in their critical section. Process can be in several (possibly many) states, such as sleeping, trying, critical; a transition relation describes how the system moves from a state to another according to whether a process is allowed to change its status. Suppose we want to verify some property of the system such as safety: for any possible sequence of transitions if the initial state is safe, so is the final one. Now, from the description of the problem, it is apparent that a state is safe if both process are not in their critical section. It would benefit the verification attempt to have a positive explicit specification of being a safe state, rather than working with an implicit negative one. Not only the number of states can be fairly large, but consider the natural extension of the same problem to n-processes: a hand-written positive specification of a state being safe can be incomplete or plain wrong. Again, over time, the number of states will increase or possibly decrease and the safety specification needs to evolve accordingly.

The bottom line is that negation is a very common connective in a specification – and rightly so, since it is one of the most basic logic operator. Formalizations that use negation are often sharper and more concise. Nevertheless, not every automated reasoning tool available nowadays is able to provide an appropriate handling of this connective. This is particularly problematic for logical frameworks based on higher-order logic with a logic programming interpretation, such as Twelf [SP98] and λProlog [NM88, Mil89a]. Whole the latter provide a very advanced unified environment for the specification, implementation and verification of deductive systems, they inherit the traditional problems with negation, which Prolog has struggled with since its inception. These problems are further augmented by some of their more beneficial features; namely by being ‘higher-order’ and being based on intuitionistic provability. Those characteristics are the main key elements of the success of those frameworks and should be preserved under every extensions. This dissertation presents an approach to endow those languages with a logically sound notion of negation without sacrifying any part of their representation power.

1.1 Logical Frameworks

A logical framework [Pfe99] is a meta-language for the specification, implementation and verification of deductive systems and their meta-theory. Deductive systems consist of axioms and rules defining derivable judgments; they can be used to specify logics and aspects of programming languages such as operational semantics, type systems, abstract machines and compilation.

Logical frameworks offer a bridge between the success of declarative programming languages (logic and functional) 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 twenty-seven equations to prove that 1 is a natural number, how many will you need to prove a real theorem?”^{1}.

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

Many logical framework have been proposed in the literature (see [Pfe99] for an overview) and many extensions are also under consideration. However, we must carefully balance the benefits that any proposed extension can bring against the complications its meta-theory would incur. We have two main issue to consider:

1. It is been argued that logical frameworks should be by design as weak as possible [dB91], in order to:

• Simplify proofs of adequacy of encodings.

• Allow effective checking of the validity of derivations.

• Reduce the complexity of proof-search.

• Inherit a treat-able unification problem.

2. At the same time logical framework must provide powerful tools to support the design process of deductive systems. Experience has shown that the strength of a logical framework is proportional to the ease it makes encodings as simple and concise as possible. The more direct is the encoding, the easier is to reason about it. One well known example is higher-order abstract syntax [PE88], which moves renaming and substitution principles to the meta-language; this avoiding to explicitly program and prove a large series of low-level results about those trivial but ubiquitous concepts. Another example is the reification of derivations as proof terms in type-theoretic languages, which reduces run-time check for correctness of derivations to type-checking in the meta-language.

The approach taken in the Twelf project is a “pay as you go” one. In other words, every extension is carefully crafted so that to be conservative on the operational and declarative semantics of the core language. Examples are the linear extension [?] or refinement types [Pfe93].

1.1.1 Negation

The aim of this thesis is to develop a framework for the synthesis of the negation of logic programs in logical frameworks such as hereditary Harrop formulae (HHF) [MNPS91] and its implementation in λProlog [NM88]. We intend this to set the basis for type-theoretic frameworks such as LF [HHP93] and its implementation Twelf [SP98] and possibly their linear refinement as Lolli [HM94] and LLF [CP96]. This approach could also be useful for generic theorem proving systems, especially ones based on higher-order logic such as Isabelle [Isa98].

1Les dernieres efforts des logiciens, in Science et Methode, p. 193.

Draft of June 20, 2000

Those systems do not provide a primitive negation operator. Indeed, constructive logics usually implement negative information as ¬A ≡ A → ⊥, where ⊥ denotes absurdity and the Duns Scoto Law is the elimination rule. Thus negative predicates have no special status; that would correspond to explicitly code negative information in a program, which is entirely consistent with the procedural interpretation of hypothetical judgments available in logical frameworks with a logic programming interpretation. However, this would not only significantly complicate goal-oriented proof search (as it is manifested in the difficulty of implementing for example, the full logic of Forum [Mil94]), but providing negative definitions seems to be particularly error-prone, repetitive and not particularly interesting; more importantly, in a logical framework we have also to fulfill the proof obligation that the proposed negative definition does behave as the complement (of its positive counterpart).

Providing a viable negation operator has an immediate practical relevance in programming in those languages, since it relieves the user from the burden of explicitly encoding negative information in the form of clauses which express the condition for a predicate not to hold. Automating the synthesis of negative information has not only an immediate practical relevance in the logic programming sense, but it may also have a rather dramatic effect on the possibility of implementing deductive systems that would prove to be too unwieldy to deal with otherwise. The synthesis of the negation of predicates such as typable, well-formed, canonical form, subsort, value etc.–as well as Prolog-like predicates such as equality, set membership and the like–will increase the amount of meta-theory that can be formalized.

Of course, the addition of negation does not change the recursive-theoretic expressive power of a language, but we claim that it does make a difference at the representation level. To bring this to the extreme, deductive systems can be expressed eventually in say Horn 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.

Traditionally, negation-as-failure (NF ) [Cla78] has been the overwhelmingly used approach in logic programming (see [AB94] for a recent survey): that is, infer ¬A if every proof of A fails finitely. The operational nature of this rule and its ultimately troublesome logical status is a serious threat to the logical frameworks’ endeavor. We will return on the topic of why NF is an absolutely inadequate way to address the issues of negation in a logical framework in Section 1.2.

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 approaches in 1.3), 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 has been attempted, with somewhat disappointing results in Harland’s thesis [Har91b].

The approach to negation that we shall investigate is transformational, also known as intensional negation, initiated in [ST84] and developed in Pisa for Horn logic. [BMPT87, BMPT90, BLLM94]. Roughly, given a clause with occurrences of negated predicates, say Q ← G, ¬P, G′, where P is an already defined atom, the aim is to derive a positive predicate, say non P which implements the complement of P, preserving operational equivalence; then, it is merely a question of replacement, yielding the negation-less clause Q ← G, non P, G′. This has the neat effect that negation and its problems are eliminated, i.e. we avoid any extension to the (meta) language. Technically, we can achieve this by transforming a Horn program into negation normal form and then by negating atoms via complementing terms, a problem first addressed in [LM87] for first-order terms.

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 computational 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” [JLLM91].

The reason why NF is so popular in the logic programming paradigm is that it essentially requires no modification to the search structure of an LP interpreter. The real question is whether it also satisfies the other aforementioned criteria. Nonetheless this is just a part of it:

“... 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 logic programming in only a special case: one manifestation of its role in logic” [Gab91].

Our answer to this plea, will be to show that, paradoxically, the best way to deal with negation in the logic programming setting is to eliminate it through transformation.

Thus where is the catch? It is a basic fact of classical propositional logic that connectives are interdefinable; more precisely, a sufficiently expressive set of sentential operators can provide, by definition, the missing ones, as an immediate consequence of their truth-value semantics. It is therefore customary and economically convenient to assume as primitive only this basis and define the others operators in terms of the former. In almost every definition negation is taken as primitive, paired either with conjunction, disjunction or implication; even those more succinct presentations based on a singleton connective as nand retain an implicit flavor of negation.

There is yet another way to address negation which 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 defined as follows:

¬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 accomplished simply by renaming. Consistency is then achieved by adding axioms that specifies that is it inconsistent to hold both p and \overline{p}, namely p ↔ ¬\overline{p} an ¬p ↔ \overline{p}.

The problem is that this does not carry immediately over to every computational logics, where the notion of negation normal form may be in itself problematic. The issue was not apparent because of the identification of logic programming with Horn programming For accident or necessity (though we now lean for the former) Horn logic imposed itself as the format in logic programming. Because of its restricted syntax classical and intutitionistic provability concide in this fragment. This entails that classical equivalences preserve the intended operational semantic of the source program. Thus negation normal form do work here, as we explain in Chapter ??

Nevertheless, this approach does not scale immediately to more expressive languages. Once we go beyond Horn logic, the intuitionistic (or ‘search-like’) interpretation becomes crucial to ensure the existence of what is commonly agreed as a reasonable interpreter for a logic programming language. Our endeavor can be paraphrased as the search for a notion of negation normal form for a significantly fragment of higher-order intuitionistic logic which is compatible with a logic programming interpretation.

It must be remarked that the issue of negation in constructivism is by no means new, but it has been considered by many problematic. One sticky point lies in the Heyting semantics of ¬A seen as a short for A → ⊥; many have expressed doubts about the epistemological status of a construction which yields the absurdum. A discussion can be found in Wansing’s monography [Wan93]. Already in its textbook [Hey56] Heyting mentions Griss’ attempt to formalize a notion of negation-less mathematics. The most well-known approach to marry a first-class notion of negation with constructivism is Nelson’s strong negation. As we will argue in Section ??, the interaction between strong negation and implication is inadequate to support the operational interpretation of HHF we are interested in.

Additionally, elimination of negation does not scale immediately to logical frameworks such as HHF, for two other re reasons:

1. The simply-typed λ-calculus is not closed under term complement.

2. There is an intrinsic tension between the Closed World Assumption (CWA), which is associated with negation, and the Open World Assumption (OWA) typical of languages with embedded implication.

Differently from the first-order case, the complement of a lambda term cannot, in general, be described by a pattern, or even by a finite set of patterns. We can isolate one basic difficulty: a pattern such as λx. E x for an existential variable E matches any term of appropriate type, while λx. E matches precisely those terms λx. M where M does not depend on x. The complement then consists of all terms λx. M such that M does depend on x. However, this set cannot be described by a pattern, or even a finite set of patterns. This formulation of the problem suggests that we should consider a calculus with an internal notion of strictness so that we can directly express that a term must depend on a given variable. We will therefore introduce a strict λ-calculus where term complement in the simply typed λ-calculus can be embedded and performed.

The second issue second one is rooted again in the fundamental difference between Horn and HHF formulae: as well known, a Horn predicate definition can be seen as an inductive definition of the same predicate. The minimality condition of inductive definitions excludes anything else which is not allowed by the base and step case(s). This corresponds in Horn logic to the existence of the least model and to the consistency of the CWA and its finitary approximation, the completion of a program [Cla78]: every atom which is not provable from a program is assumed to be false. Languages which provide embedded implication and universal quantification are instead open-ended and thus require the OWA; in fact, dynamic assumptions may, at run-time, extend the current signature and program in a totally unpredictable way. This makes it in general impossible to talk about the closure of such a program. In the literature the issue has been addressed in essentially three ways:

1. By enforcing a strict distinction between CWA and OWA predicates and applying NF only to the former [Har91b], where the latter would require minimal negation, as in [Mom92].

2. By switching to a modal logic, which is able to take into account arbitrary extensions of the program as possible worlds (see the completion construction in [GO98] for N-Prolog and [Bon94] for Hypothetical Datalog).

3. By embracing the idea of partiality in inductive definitions and using the rule of definitional reflection to incorporate a proof-theoretical notion of closure analogous to the completion [SH93, MM97].

None of those approaches are satisfactory for our purposes: most of the predicates we want to negate are open-ended; similarly, definitional reflection is not well-behaved (for example cut is not eliminable) for that very class of programs we are interested in. Moreover, we need to express the negation of a predicate in the same language where the predicate is formulated. Our solution is to restrict the set of programs we deem deniable in a novel way, so as to enforce a Regular Word Assumption (RWA): we define a class of programs whose dynamic assumptions extend the current database in a specific regular way. This constitutes a reasonable middle ground between the CWA which allows no dynamic assumption but is amenable to negation and the OWA, where assumptions are totally unpredictable. The RWA is also a promising tool in the study of the meta-logical frameworks [Sch00]. Technically, this regularity under dynamic extension is calibrated so as to ensure that static and dynamic clauses never overlap. This property extends to the negative program; in a sense, we maintain a distinction between static and dynamic information, but at a much finer level, i.e. inside the definition of a predicate. The resulting fragment is very rich, as it captures the essence of the usage of hypothetical and parametric judgments in a logical framework; namely, that they are intrinsically combined to represent scoping constructs in the object language. This is why we contend that this class of programs is adequate for the practice of logical frameworks.

1.1.2 Which logical framework

In this dissertation we work with the pattern fragment of third-order HHF; thus our results apply the same fragment of L_{λ}[Mil91], although every design decision has been influenced by the possibility to extend it to the richer language of LF and to its implementation in Twelf. We comment on this in the conclusions (Chapter ??). The latter can be seen as the dependently-typed CLP-oriented enhancement of the latter. Both share unification restricted to the pattern fragment, as well as the lack of predicate quantification.

For convenience reasons we take the liberty of decorating HHF clauses with labels that can be thought of as names. This allows us to be more concise when applying program transformations. Even though they resemble the same notation in Twelf, they lack any intrinsic meaning and will not be used as proof-terms.

In this dissertation we restrict ourselves to HHF without local variables. If we look in the usual logic programming fashion at an implicational clause as a rule where the consequent is the ‘head’ and the antecedent the ‘body’, a local variable is an essentially existential one which occurs in the body but not in the head. This is customary in the literature on elimination of negation [ST84, MPRT90]. For example the following predicates implementing graph reachability will not be allowed.

\begin{matrix}path(X, Y) ← edge(X, Y). \\ path(X, Y) ← edge(X, Z) ∧ path(Z, Y). \end{matrix}

The problem is that even Horn clauses with local variables are not closed under complementation; in fact, elimination of negation will transform those into extensionally universally quantified variables. It is a whole new topic to give an operational reading of universal quantification in this setting and to mingle it with parametric judgments. It is our feeling that the issue of local variables during complementation does not have a simple general solution. Approaches which embrace the extensional nature of universal quantification brought in by the negation of existential quantifiers [BMPT90, ABT90] are not satisfactory and robust enough to carry over to logical frameworks with intensional universal quantification.

While it is well-known that every computable function can be expressed by a Horn programs without local variables, we cannot hide that this is a somewhat severe restriction. We offer some ideas on how to partially overcome it in Subsection ??.

1.1.3 What is Failure (in a Logical Framework)?

A minimal requirement for a negation operator is that if a set of assumption Γ is consistent, it is the case that Γ ⊢ A iff not Γ ⊢ ¬A. It is a key issue how to interpret the notion of non-existence of a proof. In the logic programming tradition this has been identified with the idea of finite failure: the logic programming interpreter is run by querying a given program P with a goal G; the halting of the query without a derivation is evidence enough to assert the negation of G. This idea actually traces back to the same principle in the deductive database context, where the decision problem has a positive answer. Indeed, in this setting, the Closed World Assumption is a most natural one, since, given the large number of entries in a database, the only reasonable way to encode negation is by absence. The transfer of this idea to full logic programming [She85] has been not exactly worry-free, as the enormous literature on the subject testifies. Luckily, our requirements are somewhat different from general logic programming; in fact, in a logical framework, negation refers not to finite failure but to unprovability tout court, as we refrain from negating programs whose negation is not recursively axiomatizable: the adequacy of the representation will beak down, since there would be functions which cannot be captured by the framework. This is why we identify negation with a complement operation. This restriction, far from being an easy way out gives us the additional burden to prove that termination is preserved under every manipulation of programs.

It is clear that elimination of negation makes sense only when negation is stratified [ABW88], i.e. the negative predicates ultimately refers (in the call graph) to a positive one. We will informally adopt the generally accepted weaker notion of local stratification [AB94], when the positive dependency relies not simply on predicate names, but on ground instantiations of literals. While there may be a place in logic programming for non-stratified negation, as the emerging answer set programming paradigm [Lif99] testifies, the latter seems to be circumscribed to solving mainly combinatorial problems. This does not seem to be the a concern for a logical framework.

1.2 Negation-as-Failure

Since negative information is independent from definite 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 approach to databases. For a nice introduction see [She88, AB94]. The idea of a proof under the NF rule is a 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 ” ([Gab91] pp. 8). That motivates its intrinsic non-monotonicity: in fact, in dynamic 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 the 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 … ” ([Llo93] p. 87).

The operational nature of this rule motivates the lack of a unique semantics and some of its related troublesome features: to begin with, possible unsoundness: without run-time checks on the substitution returned by a negative open query, the final answer substitution may not be a logical consequence of the program. This is the so-called “floundering” phenomenon, the undecidable question of whether the computation will reach a negative open query and abort. Soundness is preserved only for ground queries; the flop side of the medal is that now negation is not a first-class connective, but just a test that cannot return substitutions. We review in Section 1.4.1 how and with what computational cost this can be avoided. And of course, NF is in general incomplete in general logic programming.

All of the above makes NF a suspicious candidate for a negation operator in any logic programming language, but the situation is even worse in logical frameworks. Even if we manage to isolate a well-behaved logical fragment, such as acyclic normal programs [AB90], allowing NF in a logical framework carries some additional problems. First, the meta-theory becomes really unwieldy, as both provability and unprovability must now be taken into account. The two systems would be interlinked by rules such as:

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

In a type-theoretic logical frameworkthis issue is further exacerbated by the need to deliver evidence of what a proof of a certain judgment is. The most popular way, since the Automath project [dB80], is to to see derivations as lambda terms inhabiting judgments seen as types. Although it is in principle possible to associate proof-terms to a derivation by negation-as-failure – this is implicit in the denial proof system that we present in Chapter ??, Figure ?? and ?? – the existence of (unique) canonical forms is in general impossible to achieve; and this is pretty much a death sentence for NF . In fact, in frameworks with hypothetical judgments, as recognized first by Gabbay [Gab85], the unrestricted combination of NF and embedded implication is particularly problematic, since it leads to the failure of basic logic principles such as cut-elimination. We discuss this issue in details in Section ??.

At the user level, the presence of NF in a logical framework would make adequacy theorems more difficult to establish, again because both provability and unprovability now need to be considered.

In summary the adoption of NF in a logical framework seems to be a very risky, if not hopeless road, considering its fragility already in the very simple setting of Horn clauses.

1.3 From Theorem Proving to Prolog

To set the stage, we need to say something on how logic programming and Prolog 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, ironically, 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 [Rob65]. Briefly, it is a proof procedure which proceeds by contradiction, converting a sentence to clausal form and testing for inconsistency with a version of Gentzen’s cut-rule augmented with unification. Yet, this approach has been shown to be in general non-practical. A great deal of research developed after Robinson’s breakthrough aimed at restricting the search space, while preserving completeness. 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 [Apt90]. 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, which by fixing one goal at each step, never needs to resolve two input clauses together. As far as the second point 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 choice in the side clauses, ancestors tracking and factoring. The winning strategy is to restrict the syntax of the clauses themselves; the choice fell on Horn clauses: definite clauses (that is clauses with exactly one positive literal) are interpreted as input ones, while Horn clauses with empty positive part are taken as goals. Eventually we have arrived at pure Prolog or SLD-resolution.

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 mystery, 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

begin call B_{1} call B_{2}

⋮

call B_{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 other programming language [Apt90]. Moreover, Horn logic has some nice model-theoretic properties, namely the minimum model property; it is natural to consider the latter as the declarative meaning or the intended interpretation of a program. Therefore it has been argued that we should be content with Horn logic, which seems to be a complete and reasonably efficient computational logic. However, many have argued about the difficulty to express even the easiest logical problems in a language that lacks (explicit) disjunction and negation. We share this complaint up to a certain point. We maintain the logic programming works as far as the logical and the algorithmic parts do not differ too much, and that Kowalski’s motto “Programs = Logic + Control” has shown its intrinsic limitations. Yet, we strongly share the idea that especially from a programming point of view it would 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.

There are three ways, in order of increasing complexity, to add negation to Horn logic:

• Negative atomic queries.

• Negative literals in clauses bodies.

• Negative heads.

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 [LT84].

1.4 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. Tosum up, we can isolate several (slightly overlapping) positions:

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

• 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 sub-tribes: the “logicians”, which claim that programming in Horn logic is like living with a hand tightened behind, and the “compilers” (see Sato and Tamaki. [TS84]: 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 [PG86], precompilation [LT84], change of interpreters (say connection graphs [GR87]) or, more reasonably, switching from classical logic to fragments in the intuitionistic galaxy, reviewd in Section ??.

• Finally, 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.

1.4.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 ensures that from ⊢ ∃x¬p(x) we can infer the existence of a term t such that ⊢ ¬p(t). We can roughly distinguish two approaches:

i. Program Transformation: [ST84], [FRTW88], [BMPT90].

ii. Negation by Constraints: [Wal87] for Datalog programs, [Cha88] [Cha89] and extended to CLP in [Stu95]; Fail Substitutions: [She89] [MN89].

Historically, the original attempt to deal with the issue 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 [She85], which essentially reduces evaluation to ground evaluation.

2. Try to achieve grounding by delaying as in [M]NU-Prolog [Nai86] or Sicstus [AAB^{+}], 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 more complex and historically less successful alternative is offered by the computation rules of IC-Prolog, which allow the computation of negative open queries if their positive counterpart does not bound any variable (see [Nai86], for a comprehensive analysis and references).

3. Covering the open negative query with a generator of values for the relevant variables. This is further detailed next.

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} [ABW88], say through propagation in every negative literal in the program. This is clearly infeasible, since it may result in an intractable numbers of rules, especially in an untyped setting.

A sophistication of this idea can be found in [FRTW88]: 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. 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.

Finally, the transformation approach falls in this category and is detailed in Chapter ??.

Dynamic Approaches

Chan [Cha88] is acknowledged to be the inventor of the term ’constructive’ negation in this area; his approach can be roughly characterized as mixing NF with a constraints-solving attitude. In essence it consists in evaluating a negative goal by executing its positive version and by negating the answer obtained. As in the CLP family of languages, unification and disunification are kept explicit and returned as solutions. . 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; those are addressed in a following paper ( [Cha89]), by quantifying over the answer substitutions. No proof of completeness is offered. We can offer the following rational reconstruction: the key observation is that if G is a goal and we consider the answer substitutions θ_{1}, ..., θ_{n} as equations, G ↔ ∃(θ_{1} ∨ … ∨ q_{n}) is a logical consequence of the completed database. Therefore the constructive negation rule is simply ¬G ↔ ¬∀(θ_{1} ∨ … ∨ q_{n}), where the right-hand side can be simplified by disunification. For instance given the query not(even(X)), its positive version yields the answer X = 0 ∨ ∃Y : X = s(s(Y)), whose negation is X ≠ 0 ∧ ∀Y : X ≠ ssY: its solved form is hence X = s(0), which we can regard as a more informative refinement of the answer constructive negation produces.

A generalization to constraint logic programming over arbitrary structures is given in [Stu95]; 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 [Fag97].

(E)SLDNF − S ([She89]) The finite failure case in the definition of SLDNF -resolution is modified as follows: a goal (Γ, ¬A) has a descendent θΓ, if there is a finitely failed-tree for θA, where dom(θ) ∈ F V (A). So NF can instantiate under success, i.e. negative goals may directly return substitutions: given P and G the aim is to look for a (fail) substitution θ such that 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. I am not aware of any implementation of this proposal.

This is refined in [MN89], 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 [LM87]).

1.4.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 clausal-logic, most of them are cataloged 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 me refer to [Mom92].

• N(Q)Prolog [GR84], a complete implementation of positive intuitionistic logic. By defining disjunction classically and allowing a restart rule (see nH Prolog next), Gabbay shows it to be complete for full classical logic as well.

• Negation as Inconsistency ([GS86]). Here we 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.

• Stickel’s PTTP, supplements 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.

• Loveland’s nH Prolog [RL92] incorporates case analysis in SLD-resolution, by demanding the invocation of a restart rule for every disjunctive head, until the stack of the former. Without requiring contrapositives (as in PTTP), 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.

• Another extension goes under the name of disjunctive logic programming (see [LMR92] and references therein). It aims to deal with full clausal logic by generalizing Horn clauses to disjunctive heads.

1.4.3 Proof-Theoretic Approaches to Negation and NF

In the 90’s there has been 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 [GR84]. It is customary [HSH90] to distinguish among two approaches:

1. Clauses as axioms (programs as theories) and some form of Gentzen sequent calculus to infer goals, i.e. uniform proofs systems.

2. Clauses as rules [HSH90]: Horn (and beyond) programs should be seen as set of inference rules for the derivation of (not necessarily ground) atoms.

This has the following relation with negation:

1. Minimal, intuitionistic and classical negation can be superimposed over uniform proofs [Mil89b], [Har91a], [Mom92]: 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 [MNPS91].

2. GCLA [MAK91] is based on the rule-based definitional approach to logic programming : it has intuitionistic negation built-in, applying the definiens operator to the left-hand side of a sequent. A discussion can be found in Section ??.

Stärk [Stä92] has given a sequent calculus reconstruction of NF using Clark’s equality and freeness axioms, negation (switch) ruler and cut rules. Much more is however contained in Stärk’s thesis; to quote a few, he shows that a sequent is provable in this calculus 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.

1.4.4 Outline

This dissertation is organized in two main parts which address:

• The relative complement problem.

• Clause complementation.

We start in Chapter ?? by introducing the relative complement problem; we review the existing solutions to the first-order case in the literature, namely a variant of Lassez & Marriot’s original uncover algorithm [LM87] (Section ??) and disunification [Com91] (Section ??). We then discuss in Section ?? the problems connected to extending those idea to the higher-order case, where we notice the fundamental difference between fully and partially applied terms. For the latter fragment, the simply-typed λ calculus is not closed under term complement. We remedy this by introducing the strict λ-calculus in Chapter ??. Here we list some basic properties such as the existence of canonical forms. Once we have introduced a calculus strong enough to deal with partially applied terms, Section ?? introduces a restriction of the language (“simple terms”) for which complementation is possible. The algorithm for negation is presented in Section ??; in Section ?? we give a unification algorithm for the same fragment. This completes our solution to the relative complement problems for higher-order patterns. We conclude this chapter in Section ?? by showing how to organize finite sets of simple terms into a boolean algebra. We end up this part of the dissertation reviewing related work on strictness (Section ??).

Chapter ?? sets the stage for clause complementation. First, in Section ??, we offer a rational reconstruction of the transformational approach to negation in the Horn case. Then in Section ?? and ?? we give an informal view of the complement algorithm for HHF and of the restrictions it requires by means of examples. In Section ?? we try to motivate the pragmatic adequacy of the fragment of HHF we deal with, while Section ?? reviews the state of the art on NF and intuitionistic provability.

Chapter ?? is the heart of the thesis; we first introduce the source language and its uniform proofs system in Section ??. We then establish the fundamental notion of context schema (Section ??) . This allows to enforce the Regular World Assumption (RWA), on which clause complementation is built. After formalizing the restriction to terminating program in Section ??, we present the clause complementation algorithm and the related notion of augmentation (Section ?? and ??). We then prove the main theorem (Section ?? and ??); Finally, Section ?? discuss how to give an operational semantics to our language.

We conclude the dissertation in Chapter ?? by discussing first how to lift some of the current restrictions (Section ??); then we address possible extensions, implementation issues and further future work (Section ??, ?? and ??).

1.5 Contributions and Technical Acknowledgments

The original contribution of the thesis are:

• A relative complement algorithm for higher-order patterns internalized into a strict type theory.

• A complement algorithm for a useful class of third-order hereditary Harrop formulae.

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 Twelf language and environment, but also from specific contributions which we have used (and somewhat simplified) in this thesis. Let me mention only the most recent ones: schema contexts (Schürmann [Sch00]), linear unification (Cervesato and Pfenning [CP96]), subordination (Virga [Vir99]), mode and termination analysis (Rohwedder and Pfenning [RP96]).

Finally, I want to point out that Frank Pfenning originally suggested, among others, the idea of using strict types to enforce variables occurrences and the idea of the Regular World Assumption to make clause complementation feasible.

This research has been financially supported for seven semesters by the Department of Philosophy and by a one-year scholarship from “Consiglio Nazionale delle Ricerche”, Italy.

Bibliography

[AAB^{+}] Johan Andersson, Stefan Andersson, Kent Boortz, Mats Carlsson, Hans Nilsson, Thomas Sjöland, and Johan Widn. SICStus prolog user’s manual. Technical Report T93-01, Swedish Institute of Computer Science.

[AB90] Krzysztof R. Apt and Marc Bezem. Acyclic programs. In Peter Warren, David H.D.; Szerdei, editor, Proceedings of the 7th International Conference on Logic Programming (ICLP ’90), pages 617–633, Jerusalem, June 1990. MIT Press.

[AB94] K. Apt and R. Bol. Logic programming and negation. Journal of Logic Programming, 19/20:9–72, May/July 1994.

[ABT90] D. Pedreschi A. Brogi, P. Mancarella and F. Turini. Universal quantification by case analysis. In Proc. ECAI-90, pages 111–116, 1990.

[ABW88] K. Apt, H. Blair, and A. Walker. Towards a theory of declarative knowledge. In Jack Minker, editor, Foundations of Deductive Databases, chapter 2, pages 89–148. Morgan Kaufmann, 1988.

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

[BLLM94] P. Bruscoli, F. Levi, G. Levi, and M. C. Meo. Compilative constructive negation in constraint logic programs. In Sophie Tiso, editor, Proc. Trees in Algebra and Programming - CAAP’94, 19th International Colloquium, volume 787, pages 52–76. Springer, 1994.

[BMPT87] R. Barbuti, Paolo Mancarella, Dino Pedreschi, and Franco Turini. Intensional negation of logic programs. In Proceedings ofTapsoft87, volume 259 of LNCS, pages 96–110, Austin, TX, October 1987. Springer Verlag Press.

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

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

[Cha88] D. Chan. Constructive negation based on the completed databases. In R. A. Kowalski and K. A. Bowen, editors, Proc. Fifth International Conference and Symposium on Logic Programming, pages 111–125, Seattle, Washington, August 15-19 1988.

[Cha89] D. Chan. An Extension of Constructive Negation and its Application in Coroutining. In Ewing L. Lusk and Ross A. Overbeek, editors, Proceedings of the North American Conference on Logic Programming, pages 477–496, Cleveland, Ohio, USA, 1989.

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

[Com91] H. Comon. Disunification: a survey. In J-L. Lassez and G.Plotkin, editors, Computational Logic. MIT Press, Cambridge,MA, 1991.

[CP96] Iliano Cervesato and Frank Pfenning. A linear logical framework. In E. Clarke, editor, Proceedings of the Eleventh Annual Symposium on Logic in Computer Science, pages 264–275, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press.

[dB80] N.G. de Bruijn. A survey of the project AUTOMATH. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, pages 579–606. Academic Press, 1980.

[dB91] N.G. de Bruijn. A plea for weaker frameworks. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 40–67. Cambridge University Press, 1991.

[Fag97] François Fages. Constructive negation by pruning. Journal of Logic Programming, 32(2):85–118, August 1997.

[FRTW88] Norman Foo, Anand Rao, Andrew Taylor, and Adrian Walker. Deduced relevant types and constructive negation. In Robert A. Kowalski and Kenneth A. Bowen, editors, Proceedings of the Fifth International Conference and Symposium on Logic Programming, pages 126–139, Seatle, 1988. ALP, IEEE, The MIT Press.

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

[Gab91] Dov Gabbay. Modal provability foundations for negation by failure, in extensions of logic programming. In Peter Schroeder-Heister, editor, Extensions of Logic Programming: International Workshop, Tübingen FRG, December 1989, volume 475 of Lecture Notes in Artificial Intelligence, pages 179–222. Springer-Verlag, 1991.

[GO98] Laura Giordano and Nicola Olivetti. Negation as failure and embedded implication. Journal of Logic Programming, 36(2):91–147, August 1998.

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

[GR87] Jean H. Gallier and Stan Raatz. Hornlog: A graph-based interpreter for general Horn clauses. Journal of Logic Programming, 4(2):119–155, June 1987.

[GS86] Dov M. Gabbay and Marek J. Sergot. Negation as inconsistency I. Journal of Logic Programming, 3(1):1–35, April 1986.

[Har91a] James Harland. A clausal form for the completion of logic programs. In Koichi Furukawa, editor, Proceedings of the 8th International Conference on Logic Programming, pages 711–725. MIT, June 1991.

[Har91b] James Harland. On Hereditary Harrop Formulae as a Basis for Logic Programming. PhD thesis, Edinburgh, January 1991.

[Hey56] A. Heyting. Intuitionism, an Introduction. North-Holland, Amsterdam, 3 edition, 1956.

[HHP93] Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143–184, January 1993.

[HM94] Joshua Hodas and Dale Miller. Logic programming in a fragment of intuitionistic linear logic. Information and Computation, 110(2):327–365, 1994. A preliminary version appeared in the Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, pages 32–42, Amsterdam, The Netherlands, July 1991.

[HSH90] L. Hallnas and P. Schroeder-Heister. A proof-theoretic approach to logic programming: Clauses as rules. Journal of Logic and Computation, 1(2):635-660, October 1990.

[Isa98] Isabelle. System home page, October 1998. Version 98-1.

[JLLM91] M.J. Maher J-L. Lassez and K. Marriot. Elimination of negation in term algebras. In A. Tarlecki, editor, Mathematical Foundations of Computer Science, pages 1–16, Berlin, jul 1991. Springer-Verlag.

[Kah87] Gilles Kahn. Natural semantics. In Proceedings of the Symposium on Theoretical Aspects of Computer Science, pages 22–39. Springer-Verlag LNCS 247, 1987.

[Lif99] Vladimir Lifschitz. Answer set planning. In D. De Schreye, editor, Proceedings of the International Conference on Logic Programming (ICLP’99), pages 23–35. MIT Press, 1999.

[Llo93] J. W. Lloyd. Foundations of Logic Programming, Second Extended Edition. Springer-Verlag, 1993.

[LM87] J.-L. Lassez and K. Marriot. Explicit representation of terms defined by counter examples. Journal of Automated Reasoning, 3(3):301–318, September 1987.

[LMR92] J. Lobo, J. Minker, and A. Rajasekar. Foundations of Disjunctive Logic Programming. MIT press, Cambridge, Massachusetts, 1992.

[LT84] J. W. Lloyd and R. W. Topor. Making PROLOG more expressive. LOGIC PROGRAM. (USA) ISSN: 0743-1066, 1(3):225–40, October 1984.

[Mak87] Johann A. Makowsky. Why Horn formulas matter in computer science: Initial structures and generic examples. Journal of Computer and System Sciences, 34:266–292, 1987.

[MAK91] L. Hallnass Martin Aronson, L-H. Eriksson and P. Kreuger. A survey of GCLA: a definitional approach to logic programming. In Peter Schroeder-Heister, editor, Proceedings of the First International Workshop on Extensions of Logic Programming, volume 1050 of 475, pages 19–34, Berlin, March28–30 1991. Springer.

[Mil89a] Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. In Peter Schroeder-Heister, editor, Proceedings of the International Workshop on Extensions of Logic Programming, pages 253–281, Tübingen, Germany, 1989. Springer-Verlag LNAI 475.

[Mil89b] Dale Miller. A logical analysis of modules in logic programming. Journal of Logic Programming, 6(1-2):79–108, January 1989.

[Mil91] Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497–536, 1991.

[Mil94] Dale Miller. A multiple-conclusion meta-logic. In S. Abramsky, editor, Ninth Annual IEEE Symposium on Logic in Computer Science, pages 272–281, Paris, France, July 1994.

[MM97] Raymond McDowell and Dale Miller. A logic for reasoning with higher-order abstract syntax: An extended abstract. In Glynn Winskel, editor, Proceedings of the Twelfth Annual Symposium on Logic in Computer Science, pages 434–445, Warsaw, Poland, June 1997.

[MN89] J. Maluszyński and T. Näslund. Fail Substitutions for Negation as Failure. In Ewing L. Lusk and Ross A. Overbeek, editors, Proceedings of the North American Conference on Logic Programming, pages 461–476, Cleveland, Ohio, USA, 1989.

[MNPS91] Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991.

[Mom92] Alberto Momigliano. Minimal negation and hereditary Harrop formulae. In Anil Nerode and Mikhail Taitslin, editors, Proceedings of Logical Foundations of Computer Science (Tver ’92), volume 620 of LNCS, pages 326–335, Berlin, Germany, July 1992. Springer.

[MPRT90] Paolo Mancarella, Dino Pedreschi, Marina Rondinelli, and Marco Tagliatti. Algebraic properties of a class of logic programs. In Saumya Debray and Manuel Hermenegildo, editors, Proceedings of the 1990 North American Conference on Logic Programming, pages 23–39, Austin, 1990. ALP, MIT Press.

[Nai86] Lee Naish, editor. Negation and Control in Prolog, volume 238 of Lecture Notes in Computer Science. Springer Verlag, 1986.

[NM88] Gopalan Nadathur and Dale Miller. An overview of λProlog. In Kenneth A. Bowen and Robert A. Kowalski, editors, Fifth International Logic Programming Conference, pages 810–827, Seattle, Washington, August 1988. MIT Press.

[PE88] Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN ’88 Symposium on Language Design and Implementation, pages 199–208, Atlanta, Georgia, June 1988.

[Pet81] G. L. Peterson. Myths about the mutual exclusion problem. Information Processing Letters, 12(3):115–116, June 1981.

[Pfe93] Frank Pfenning. Refinement types for logical frameworks. In Herman Geuvers, editor, Informal Proceedings of the Workshop on Types for Proofs and Programs, pages 285–299, Nijmegen, The Netherlands, May 1993.

[Pfe99] Frank Pfenning. Logical frameworks. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning. Elsevier Science Publishers, 1999. In preparation.

[PG86] David L. Poole and Randy Goebel. Gracefully adding negation and disjunction to Prolog. In Ehud Shapiro, editor, Proceedings of the Third International Conference on Logic Programming, Lecture Notes in Computer Science, pages 635–641, London, 1986. Springer-Verlag.

[RL92] David W. Reed and Donald W. Loveland. A comparison of three Prolog extensions. Journal of Logic Programming, 12(1-2):25–50, January 1992.

[Rob65] J. Alan Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23–41, January 1965.

[RP96] Ekkehard Rohwedder and Frank Pfenning. Mode and termination checking for higher-order logic programs. In Hanne Riis Nielson, editor, Proceedings of the European Symposium on Programming, pages 296–310, Linköping, Sweden, April 1996. Springer-Verlag LNCS 1058.

[Sch00] Carsten Schürmann. Automating the meta theory of deductive systems. PhD thesis, Carnegie Mellon University, 2000.

[SH93] Peter Schroeder-Heister. Rules of definitional reflection. In M. Vardi, editor, Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science, pages 222–232, Montreal, Canada, June 1993.

[She85] John C. Shepherdson. Negation as failure II. The Journal of Logic Programming, 2(3):185–202, Oktober 1985.

[She88] J. C. Shepherdson. Negation in logic progamming. In J. Minker, editor, Found. of Deductive Databases and Logic Programming, page 19. Morgan Kaufmann, San Mateo, CA, 1988.

[She89] J. C. Shepherdson. A sound and complete semantics for a version of negation as failure. Theoretical Computer Science, 65(3):343–371, July 1989.

[SP98] Carsten Schürmann and Frank Pfenning. Automated theorem proving in a simple meta-logic for LF. In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction (CADE-15), pages 286–300, Lindau, Germany, July 1998. Springer-Verlag LNCS 1421.

[ST84] T. Sato and H. Tamaki. Transformational logic program synthesis. In International Conference on Fifth Generation Computer Systems, 1984.

[Stä92] R. F. Stärk. The Proof Theory of Logic Programs with Negation. PhD thesis, University of Berne, Switzerland, 1992.

[Stu95] Peter J. Stuckey. Negation and constraint logic programming. Information and Computation, 118(1):12–33, April 1995.

[TS84] H. Tamaki and T. Sato. Unfold/fold transformation of logic programs. In Sten-Åke Tärnlund, editor, Proceedings of the Second International Conference on Logic Programming, pages 127– 138, Uppsala, 1984.

[Vir99] Roberto Virga. Higher-Order Rewriting with Dependent Types. PhD thesis, Department of Mathematical Sciences, Carnegie Mellon University, 1999. Forthcoming.

[Wal87] M. Wallace. Negation by constraints: A sound and efficient implementation of negation in deductive databases. In Proceedings of the Fifth International Conference and Symposium on Logic Programming, pages 253–263, San Francisco, August - September 1987. IEEE, Computer Society Press.

[Wan93] Heinrich Wansing. The logic of information structures, volume 681 of Lecture Notes in Artificial Intelligence and Lecture Notes in Computer Science. Springer-Verlag Inc., New York, NY, USA, 1993. Revision of the author’s doctoral thesis (Fachbereich Philosophie und Sozialwissenschaften I of the Free University of Berlin).

[WM91] Larry Wos and William McCune. Automated theorem proving and logic programming: A natural symbiosis. Journal of Logic Programming, 11(1):1–53, July 1991.