**ICCL Summer School 2004
Proof Theory and Automated Theorem Proving
and
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**

**Term Rewriting Systems**

Franz Baader (TU Dresden)**Deep Inference and the Calculus of Structures**

Alessio Guglielmi (TU Dresden)**Game Semantics and Its Applications**

C.-H. L. Ong (Oxford)

On June 14 Wolfgang Bibel (TU Darmstadt and Un. British Columbia) gives an invited lecture on

Transition LogicOn 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**

**Deduction Modulo**

Claude Kirchner (Loria & INRIA, Nancy)**Logic Considered as a Branch of Geometry**

François Lamarche (Loria & INRIA, Nancy)**Proofs as Programs**

Michel Parigot (CNRS - Université Paris 7)**Automated Reasoning for Substructural Logics**

John Slaney (NICTA, Canberra and Australian National University)**Automated Theorem Proving for Classical Logics**

Andrei Voronkov (Manchester)

On June 22 Roy Dyckhoff (St Andrews) gives an invited lecture on

Sequent Calculi for Some Non-classical Logics.

**Transition Logic**

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 decorations—in 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 logic—specifically, 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.

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.

**Deduction Modulo**

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)

Room 350 for lectures and room 357 for coffee-breaks

Computer Science Department

Hans-Grundig-Str. 25

01307 Dresden

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**

CoursesWorkshopMON TUE WED THU FRI SAT 9:00-10:00 OngOngOngBaaderWorkshopWorkshop10:00-10:15 break break break break 10:15-11:15 OngOngBaaderBaader11:15-11:30 break break break break 11:30-12:30 GuglielmiGuglielmiGuglielmiGuglielmi12:30-13:45 lunch lunch excursion lunch lunch 13:45-14:45 BibelRonchi Della RoccaWorkshopWorkshop14:45-15:00 break break 15:00-16:00 BaaderBaader16:00-16:15 break 16:15-17:15 Guglielmi

**Week 2: June 21-25, 2004**

CoursesMON TUE WED THU FRI 9:00-10:00 SlaneySlaneyKirchnerSlaney10:00-10:15 break break break break 10:15-11:15 KirchnerKirchnerKirchnerKirchnerSlaney11:15-11:30 break break break break break 11:30-12:30 VoronkovVoronkovVoronkovParigotSlaney12:30-13:45 lunch lunch excursion lunch lunch 13:45-14:45 LamarcheDyckhoffParigotParigot14:45-15:00 break break break break 15:00-16:00 LamarcheLamarcheLamarcheLamarche16:00-16:15 break break break break 16:15-17:15 ParigotParigotVoronkovVoronkov

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

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.

**Organisation**

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.