Chapter 1

Introduction

1.1 Overview 1.2 Preliminaries

Definitions and conventions, two words on lpand transformation on them

1.3 Motivations

1.3.1 holp

Taken from Nadathur & Miller survey

1.3.2 Elf

From Frank‘s book 2 CHAPTER 1. INTRODUCTION

What is Negation

A cursory look to the formulation of classical and constructive negation, possibly using Gabbay and something from Curry‘s textbook.

2.1 Minimal Negation

2.2 Intuitionistic Negation

2.2.1 Negation as inconsistency

Gabbay

2.2.2 Structured Negation as inconsistency

Gabbay & Wansing

2.3 Intermediate logics

How negation behaves in constructive systems between Int and C (Ornaghi-Miglioli)

2.3.1 strong negation

(Nelson-Wansing)

2.4 CLASSICAL NEGATION

2.5 NF

Dickhoff and Harland unprovability sequent system

2.5.1 Formulation in Analytical Calculi

A common way to look to sequents is as a proof-search formulation of natural deduction; yet this may enforce some choices (as singleton conclusion) that appears to be limiting for a in-depth analysis of the role of negation.

Intuitionistic PC (IPC)

They come in two flavors: sequents (Gentzen) and tableaux (Beth, ST), coming respectively from a syntactic and semantic standpoint. Consider positive IPC (no negation even defined, no absurdity). Add negation to sequents (SQ); options:

• SQ^{⊥} negation defined and DSL rule:

• SQ^{¬} negation primitive:

• parametric negation (Frank-Kleene) and DSL rule:

• negation with certain falsum (Miglioli-Ornaghi)

On Duplication

Not^{1} all duplications are the same: as far as IPC can go two ways: LJ ⇒ LJT or ST ⇒ ST^{F_{c}} ⇒ ST^{F_{c}}T (T for terminating).

NF as unprovability

1may be skipped as irrelevant

Negation in logic Programming

From my master thesis

3.1 Overview of /in /

3.1.1 Constructive negation

Chan-Stuckey-Drabent: the constraint approach, in the likelyhood that we have constraints as a residue of the transformation

3.2 Negation and Uniform Proofs

From Frank‘s notes on ATP and some paper of mine

3.2.1 NF, and termination

From Frank & Ekk. paper on modes and Bol‘s thesis: when a logic program is a decision procedure; finite and infinite failure, negation of r.e. logic programs 6 CHAPTER 3. NEGATION IN LOGIC PROGRAMMING

The state of the art on the transformation

This will be the final stage of the document I gave you

4.1 Complement Problems 4.2 Background on fo-(dis)unification 4.3 Equational Problems and Disunification 4.4 Putting it together 4.5 The Trouble with Local Variables 4.6 Logic Programming and Universal Quan-

tification

4.6.1 Covering 4.6.2 More on DCA 4.6.3 The CASE algorithm

8CHAPTER 4. THE STATE OF THE ART ON THE TRANSFORMATION

HO-Extensions

5.1 horn logic

Two sides: ‘Functional‘ l-terms as data structure (abstract syntax):

Distinguish the two langages

5.1.1 HH- without predicate quantifications 5.1.2 Pattern Disunification and Transformation

Hopefully improving on Lugiez algorithm

5.1.3 Beyond Pattern for HH-

Have some experimental evidence of the behavior (termination, residues) of disunification for typical programs

5.1.4 HH with predicate quantification

5.2 Ur-ELF

a higher-order language extending HH- with , Π, but essentially first-order as quantification is concerned and not type-theoretic: Thru the l-cube get to 10 APPENDIX . HO-EXTENSIONS

5.3 ELF 5.4 CC .1 Appendix: Regular Splitting

Taken from my paper(s) with Mario; presenting an alternative, prooftheoretic transformation technique.