[Prev][Next][Index][Thread]
Two papers on abstract logic programming
Hello,
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>.
Ciao,
-Paola
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