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

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).

Slides

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

Monday 21.2 afternoon

Tuesday 22.2 morning

Tuesday 22.2 afternoon

Wednesday 23.2 morning

Wednesday 23.2 afternoon

28.2.2005Alessio Guglielmiemail