ICCL Summer School 2004
Proof Theory and Automated Theorem Proving
PCC Workshop 2004
Technische Universität Dresden
June 14-25, 2004
Call for Participation
This two-week meeting consists of two integrated parts, a summer school and a workshop, aimed at graduate students and researchers. The themes for the summer school are proof theory and automated theorem proving, the workshop is about proof, computation and complexity. As in the summer schools at TU Dresden in 2002 and 2003 and in the previous editions of the PCC workshop, people from distinct but communicating communities will gather in an informal and friendly atmosphere.
We ask for a participation fee of 200 EUR. We request registration before May 10, 2004; please send an email to PTEvent@ICCL.TU-Dresden.DE, making sure you include a very brief bio (5-10 lines) stating your experience, interests, home page (if available), etc. It will be possible for some students to present their work: please indicate in your application if you would like to do so and give us some information about your proposed talk.
We will select applicants in case of excessive demand. A limited number of grants covering all expenses is available, please indicate in your application if the only possibility for you to participate is via a grant. Applications for grants must include an estimate of travel costs and they should be sent together with the registration. We will provide assistance in finding an accommodation in Dresden.
Week 1, June 14-17: courses on
On June 14 Wolfgang Bibel (TU Darmstadt and Un. British Columbia) gives an invited lecture on Transition Logic
On June 15 Simona Ronchi Della Rocca (Torino) gives an invited lecture on A Logic for Intersection Types
June 17-19: workshop
For more details, please consult the workshop web page.
Week 2, June 21-25: courses on
On June 22 Roy Dyckhoff (St Andrews) gives an invited lecture on Sequent Calculi for Some Non-classical Logics.
Abstracts of Invited Lectures
Wolfgang Bibel (TU Darmstadt and Un. British Columbia)
The talk addresses the problem of how to integrate into a classical logical framework transitions which change the knowledge state of an agent. The transition logic achieves this integration by defining a deductive relationship among formulas for a partially order set of transitions. This novel integration is closer to human reasoning as experienced in natural language use than previous approaches to this fundamental problem. It provides a unified framework for practical reasoning with the potential of a full exploitation of the maturing techniques from classical deduction and from special applications such as planning, explanation, diagnosis, nonmonotonic reasoning, and others.
A Logic for Intersection Types
Simona Ronchi Della Rocca (Torino)
The intersection type assignment system (IT) is a set of rules for assigning types to terms of the untyped lambda-calculus. The types of IT are built from the connectives -> (which behaves like the intuitionistic implication) and ^ (called "intersection").
IT was introduced in 1980 by Mariangiola Dezani and Mario Coppo, in order to enhance the typability power of the Curry type assignment system. The system characterizes exactly the strong normalization property of lambda-terms. It is well known that derivations in Intersection Types (IT) form a strict subset of deductions in Intuitionistic Logic (LJ)up to term decorationsin the sense that IT imposes a meta-theoretical restriction on proofs: conjunction can be introduced only between derivations that are synchronized with respect to the implication.
The talk will present a proof-theoretical justification for IT. In particular, the relationship between the intersection connective and the intuitionistic conjunction will be explored. For this purpose, a new logical system called Intersection Synchronous Logic (ISL) has been defined. ISL proves properties of sets of deductions of the implication-conjunction fragment of LJ.
The main idea behind ISL is the decomposition of the intuitionistic conjunction into two connectives, one with synchronous and the other with asynchronous behavior.
ISL enjoys both the strong normalization and sub-formula properties as well as that the Intersection Type assignment can be viewed as standard term decoration of ISL.
Sequent Calculi for Some Non-classical Logics
Roy Dyckhoff (St Andrews)
We review the different flavours of sequent calculus, organised for root-first proof search, for logics other than classical logicspecifically, intuitionistic logic, modal logics, intermediate logics such as Goedel-Dummett logic and Jankov logic, and some connections between them. Calculi with both labelled and unlabelled formulae are considered. Topics such as termination (of search) and backtracking (and its avoidance) are emphasised, with some related remarks on complexity.
SlidesSame as powerpoint presentation
Abstracts of Courses
Disclaimer: "The works were partially funded by the Information Society Technologies programme of the European Commission, Future and Emerging Technologies under the IST-2001-33123 CoLogNET project."
Term Rewriting Systems
Franz Baader (TU Dresden)
Term rewriting systems can be used to compute in structures that are defined by equations. They are thus an important tool in automated deduction, algebraic specification, and functional programming. The course introduces important properties such as termination and confluence of term rewriting systems, describes methods for proving termination and confluence, and shows how Knuth-Bendix completion can (sometimes) be used to make non-confluent term rewriting systems confluent.
Deep Inference and the Calculus of Structures
Alessio Guglielmi (TU Dresden)
The Calculus of Structures is a proof-theoretical formalism motivated by computation. Its most direct analogue is Gentzen's Sequent Calculus. We know that systems in the Sequent Calculus can be interpreted computationally, in the proof-normalisation-as-computation and proof-search-as-computation paradigms. Many aspects of computation are not managed satisfactorily by the Sequent Calculus, especially some important for distributed computation, like locality, atomicity and several kinds of modularity. This holds for all logics expressed in the Sequent Calculus, including, e.g., Linear Logic.
The Calculus of Structures addresses these problems in a radically new, purely proof-theoretical foundation, based on the principles of deep inference and top-down symmetry. We express classical, linear, modal logics, and several variants thereof, and their deductive systems are as simple as those in the Sequent Calculus, but possess the desired computational properties. This new proof theory is richer than the old one, e.g., there are new interesting notions of normalisation.
(web site on the Calculus of Structures)
Game Semantics and Its Applications
C.-H. L. Ong (Oxford)
Game semantics is a way of giving meanings to programming languages (and to logical systems) using basic and intuitive notions of game playing. The approach goes back to Kleene and Gandy in one tradition, and to Kahn and Plotkin, and Berry and Curien in another. The former was essentially Kleene's programme to characterize higher-type sequential computation in terms of a protocol for game playing, and the latter was motivated by the Full Abstraction Problem for (Scott's prototypical language) PCF. Compared to other semantics of programming languages, the striking features of game semantics are that it is denotational (and so admits compositional methods) and yet has clear operational content; further it gives rise to accurate models for programming languages covering a wide range of features including block-allocated assignable variables, dynamic generation of local names, various control, non-deterministic, probabilistic and concurrent constructs.
This introductory lecture course presents the fully abstract model for PCF and Idealized Algol, and concludes with a survey of a recent algorithmic development in game semantics that is concerned with applications to software model checking and program analysis.
Claude Kirchner (Loria & INRIA, Nancy)
Deduction and computation are two fundamental concepts that appear in all domains of computer science as for example when mechanizing reasoning or when programming with constraints or when embedding specific knowledge about a given domain.
As computation and deduction interact in a very integrated way, they cannot be studied nor used in independent ways. Deduction Modulo is a general way to study and use the in depth combination of computation and deduction.
This lecture will present deduction modulo in general as well as in some of its important instances like rewriting modulo equational theories. We will also show some of its applications to proof assistants as well as to programming languages design and implementation.
Logic Considered as a Branch of Geometry
François Lamarche (Loria & INRIA, Nancy)
Our course will be built on a series of correspondences between geometric and logical constructions. Here we give the three main ones, that will form the backbone of the course.
Dependent type -- Indexed space ("fibration")
Model of propositional intuitionistic logic -- lattice of opens of a topological space
Model of higher-order intuitionistic logic -- category of sheaves over a topological space.
The presentation will illustrate many ideas of category theory by concrete examples.
Proofs as Programs
Michel Parigot (CNRS - Université Paris 7)
Cut elimination plays a central role in proof theory. It allows in particular to give computational interpretations of logical deduction systems: proofs become programs whose computational mechanim is precisely a cut elimination procedure.
The course will be a very elementary presentation of some basic questions of the field: constructive existence, the basic correspondance between intuitionistic proofs and functional programs, computational interpretations of classical logic, proofs of strong normalisation for confluent and non confluent interpretations.
Automated Reasoning for Substructural Logics
John Slaney (NICTA, Canberra and Australian National University)
This course concerns the application of automated reasoning techniques to logics broadly in the substructural family, such as linear logic, affine logic, relevant logic or the like. It is naturally easy, given a cut-free sequent calculus presentation with an algorithmic flavour of a system of logic, to generate a program that searches for proofs in the logic, and given a proof of termination for some fragment of the logic this generally yields a decision procedure for that fragment. What is less easy is to produce an implementation that works acceptably in a practical sense and is actually useful.
In this course, rather than examine decidability or complexity results for substructural logics and their fragments, we concentrate on the practicalities of automated reasoning with respect to substructural systems, highlighting the questions "What is this automated reasoner useful for?" and "What are the issues affecting its performance?" The reasoning in question is not confined to theorem proving, but includes the generation of models of given logics satisfying given additional constraints. Case studies of real research software are presented, and it is hoped that students will have the opportunity of some hands-on experience with these.
Automated Theorem Proving for Classical Logics
Andrei Voronkov (Manchester)
Venue and Facilities
Room 350 for lectures and room 357 for coffee-breaks
Computer Science Department
Tel.: +49 (351) 463 38340 (Sylvia Epp, secretary)
Every day room 350 will be available for discussions and talks until 20:00.
Rooms 106 and 108 have freely available Unix workstations: participants are given a personal account for the duration of the school.
In this period Dresden is hot and possibly windy; sometimes it rains.
See here how to reach us.
Registration starts at 8:30 on Monday, June 14, in front of the lecture room.
Week 1: June 14-19, 2004
Courses Workshop MON TUE WED THU FRI SAT 9:00-10:00 Ong Ong Ong Baader Workshop Workshop 10:00-10:15 break break break break 10:15-11:15 Ong Ong Baader Baader 11:15-11:30 break break break break 11:30-12:30 Guglielmi Guglielmi Guglielmi Guglielmi 12:30-13:45 lunch lunch excursion lunch lunch 13:45-14:45 Bibel Ronchi Della Rocca Workshop Workshop 14:45-15:00 break break 15:00-16:00 Baader Baader 16:00-16:15 break 16:15-17:15 Guglielmi
Week 2: June 21-25, 2004
Courses MON TUE WED THU FRI 9:00-10:00 Slaney Slaney Kirchner Slaney 10:00-10:15 break break break break 10:15-11:15 Kirchner Kirchner Kirchner Kirchner Slaney 11:15-11:30 break break break break break 11:30-12:30 Voronkov Voronkov Voronkov Parigot Slaney 12:30-13:45 lunch lunch excursion lunch lunch 13:45-14:45 Lamarche Dyckhoff Parigot Parigot 14:45-15:00 break break break break 15:00-16:00 Lamarche Lamarche Lamarche Lamarche 16:00-16:15 break break break break 16:15-17:15 Parigot Parigot Voronkov Voronkov
Dresden, on the river Elbe, is one of the most important art cities of Germany. You can find world-class museums and wonderful architecture and surroundings. We organise trips and social events.
Details on the cultural program
Accommodation and Public Transports
Some hotels and apartment agencies offer accommodation to participants. In general, you should mention the magic words `Summer School at TU Dresden´ in order to have special prices applied. All suggested places are conveniently connected by public transportation to the summer school and workshop venue. Please act fast and no later than May 25, because it's very difficult to find rooms in this period of the year in Dresden.
Complete accommodations list and information on public transports
62 people participated to the summer school and workshop.
List of participants
This event is organized by the International Center for Computational Logic (ICCL), Paola Bruscoli, Birgit Elbl, Sylvia Epp, Bertram Fronhöfer, Axel Großmann, Alessio Guglielmi, Steffen Hölldobler, Reinhard Kahle, Aning Song and Mariana Stantcheva; it is sponsored by Deutscher Akademischer Austausch Dienst (DAAD), under the program `Deutsche Sommer-Akademie´, Graduiertenkolleg 334 (Specification of discrete processes and systems of processes by operational models and logics), and CoLogNet. This event has been partially funded by the Information Society Technologies programme of the European Commission, Future and Emerging Technologies under the IST-2001-33123, CoLogNET project.
The event really took place.