文档介绍：IntroductiontoSequentCalculusand
AbstractLogicProgramming
CourseNotes
These notes refer to an old course, they are not
AlessioGuglielmi meant for DS 2001!
TechnischeUniversit¨atDresden
Hans-Grundig--01062Dresden-Germany
Alessio.******@-
1IntroductionandAimoftheCourse
,like
innaturaldeduction,directlymodelsyntacticalpropertiesoflogicalcon-
nectives,asopposedtotheHilbert-Tarskitraditionofusingaxiomstothis
purpose.
Inrecentyears,munitystartednewandbroadstudies
inthesyntacticalrealm,ethemainlogical
,ithasbeenprovena
veryeffectivewaytostudyanddesignnewlogicprogramminglanguages,
whosemorematureoffspringisnowλ-
ismuchclosertooperationalsemanticsthantheoldmethodsbasedon
traditionallogicalsemantics,likemodeltheory,sothenewsequentcalculus
perspectivepermitseasierandmorenaturaldevelopmentoflanguages.
Purposeofthisshortcourseistopresentthefundamentalsofsequent
calculussyntax,parisontothemorefamiliarnaturaldeductionsyn-
-
coursewillbetheuseofsequentcalculusasawaytodesignlogicpro-
presentedandexamplesoflanguagesinthissettingwillbegiven.
Thiscourseistobeconsideredintroductorytoacourseinλ-Prolog
whichshouldbeofferednextyear.
2 Alessio Guglielmi
2 Study Material, Final Exam and Exercises
After each lecture a new handout is given to the students covering the
last topics. The examination material is exactly what is covered in these
notes, except where explicitly indicated. The exercises in the notes are
representative of what shall be found in the final exam.
It is expected that students read all the material which is cited in
the notes, which are rather sketchy, but what is not in the notes is not
required to plete the examination. These notes are not
independent, they