Two papers on abstract logic programming


the following two papers might be interesting for people in the types 
and proof theory lists. Feedback is very welcome. Both papers are 
accessible from <http://alessio.guglielmi.name/res/sc>.



A Tutorial on Proof Theoretic Foundations of Logic Programming
Paola Bruscoli and Alessio Guglielmi

Abstract logic programming is about designing logic programming 
languages via the proof theoretic notion of uniform provability. It 
allows the design of purely logical, very expressive logic 
programming languages, endowed with a rich meta theory. This tutorial 
intends to expose the main ideas of this discipline in the most 
direct and simple way.

Invited tutorial at ICLP '03

On Structuring Proof Search for First Order Linear Logic
Paola Bruscoli and Alessio Guglielmi

We start from the Forum presentation of first order linear logic to 
design an equivalent system for which proof search is highly 
structured. We restrict formulae to a language of clauses and goals, 
without losing expressivity, in such a way that formulae have the 
same structure of Forum sequents. This means having a very big 
generalised connective that suffices for all of linear logic. We can 
then design a system with only two big rules, a left one and a right 
one. The behaviour of such system in proof search is operationally 
interesting and makes it suitable for further semantic 
investigations. We test the mutual harmony of the new rules by 
showing a cut elimination theorem.

Paper at LPAR '03
Paola Bruscoli
Technische Universitaet Dresden