A Tutorial on Proof Theoretic Foundations of Logic Programming

10 September 2003 Invited tutorial at ICLP ’03ATutorialonProof TheoreticFoundationsof LogicProgrammingPaola Bruscoli and Alessio GuglielmiTechnische Universita¨t DresdenHans-Grundig-Str. 25 - 01062 Dresden - GermanyPaola.Bruscoli@Inf.TU-Dresden.DE, Alessio.Guglielmi@Inf.TU-Dresden.DEAbstract Abstract logic programming is about designing logic programming languagesvia the proof theoretic notion of uniform provability. It allows the design of purelylogical, 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 andsimple way.1 IntroductionLogicprogrammingistraditionallyintroducedasanapplicationoftheresolutionmethod. A limitation of this perspective is the difficulty of extending the purelanguageofHornclausestomoreexpressivelanguages,withoutsacrificinglogicalpurity.After the work on abstract logic programming of Miller, Nadathur andother researchers (see especially [7, 8, 6]), we know that this limitation canlargely be overcome by looking at logic programming from a proof theoreticperspective, through the idea of uniform provability. This way, one can makethe declarative and operational meaning of logic programs coincide for largefragments of very expressive logics, like several flavours of higher order logicsand linear logics. For these logics, proof theory provides a theoretical support,which is ‘declarative’ even in absence of a convenient ...