**ICCL Workshop
Proof Theory 2005
Technische Universität Dresden
February 21-23, 2005**

This meeting is dedicated to deep inference and related matters. The meeting will mostly take place on February 22 and 23.

**Participants**

- Kai Brünnler (Bern)
- Paola Bruscoli (TU Dresden)
- Alessio Guglielmi (TU Dresden)
- Yves Guiraud (Marseille)
- Robert Hein (TU Dresden)
- Ozan Kahramanogullari (Leipzig)
- Richard McKinley (Bath)
- Charles Stewart (TU Dresden)
- Lutz Straßburger (Saarbrücken)
- Alwen Tiu (LORIA, Nancy)

**Talks**

Scenes from a Marriage

Kai Brünnler (Bern) and Alessio Guglielmi (TU Dresden)There is tension between a deductive definition of a bureaucracy-free formalism and its term calculus.

Derivations as 3-Dimensional Objects

Yves Guiraud (Marseille)Higher-dimensional rewriting provides a categorical setting to interpret derivations as geometry-flavoured objects, together with a unifying theory for the calculus of structures and formalisms A and B (and many rewriting systems).

In the calculus of structures, derivations are 1-dimensional: this is why there is much bureaucracy. I will show how one can build one (resp. two) new composition(s) on derivations: this leads to a 2(resp. 3)-dimensional interpretation of these objects and yields the same identifications of proofs as required for formalism A (resp. B).

Replacing Labelling Through Depth

Robert Hein (TU Dresden)

Reducing the Non-Determinism in Proof Search in System BV

Ozan Kahramanogullari (Leipzig)

System BV is NP-Complete

Ozan Kahramanogullari (Leipzig)

From Hyperdoctrines for Natural Deduction to Classical Doctrines(1)

Richard McKinley (Bath)

Categories, Coherence and Deep Inference(2)

Richard McKinley (Bath)

A Prolegomena to a Unified Syntactical and Semantical Theory of Analytic Modal Logic

Charles Stewart (TU Dresden)

A Local System for Intuitionistic Logic(1)

Alwen Tiu (LORIA, Nancy)This paper presents a system for intuitionistic logic in which all the rules are local, in the sense that, in applying the rules of the system, one needs only a fixed amount of information about the logical expressions involved. The main source of non-locality is the contraction rule. We show that the contraction rule can be restricted to the atomic one, provided we employ {\em deep-inference}, i.e., to allow rules to apply anywhere inside logical expressions. However, the use of deep-inference and the asymmetry of the logic give rise to the context-dependency of the rules. We further show that this context dependency can be removed by introducing polarities into logical expressions. We present the system in the calculus of structures, a proof theoretic formalism which supports deep-inference. This system is shown to be sound and complete with respect to Gentzen's LJ and an equivalent notion of cut-elimination is proved.

The Need for Deep Inference(2)

Alwen Tiu (LORIA, Nancy)

**Venue**

Room 357

Computer Science Department

Hans-Grundig-Str. 25

01307 Dresden

Tel.: +49 (351) 463 38340 (Sylvia Epp, secretary)

See here how to reach us.

**Timetable**

- 14:00-16:00 Richard McKinley (1)

**Tuesday 22.2 morning**

- 9:30-11:00 Yves Guiraud
- 11:00-12:30 Kai Brünnler and Alessio Guglielmi

**Tuesday 22.2 afternoon**

- 14:00-14:45 Charles Stewart
- 14:45-15:30 Robert Hein
- 15:30-16:30 Alwen Tiu (1)

**Wednesday 23.2 morning**

- 9:30-11:00 Alwen Tiu (2)
- 11:00-12:30 Ozan Kahramanogullari

**Wednesday 23.2 afternoon**

- 14:00-15:45 Richard McKinley (2)
- 15:45-17:30 Yves Guiraud
- 17:30-20:00 Kai Brünnler

28.2.2005Alessio Guglielmiemail