Proof Theory Meeting in Bath
6–8 July 2006
People and Dates
plus the locals:
Contributions
6 July 2006
10–12:10 Kai Brünnler
- Discussion on bureaucracy.
12:10–12:30 Lutz Straßburger
- Deep inference system for second order propositional MLL.
14–15:00 Alessio Guglielmi
- He asked for feedback on a very general definition of deep-inference formalism, conceived with Michel Parigot. The ambition is to make an important step towards what I call `deductive nets´, i.e., formalisms which are deductive (like all deductive systems) and bureaucracy-free (like proof-nets, which are not deductive, though).
15–16:00 Kai Brünnler
- Deep sequents and modal logics.
16–17:00 Robert Rothenberg
- Talk about `Mix rules in hypersequent calculi´. The focus of the talk was on the calculus GŁ for Łukasiewicz logic, for which mix could be eliminated using a calculus GŁ2. (I conjecture that similar calculi can be derived from other calculi with mix rules.) Structural proofs of the completeness of GŁ2 are difficult since (1) mix rules have no active/principal formulae (2) hypersequent rules with multiple active components in the premisses make derivation rewriting problematic.
17–17:15 François Lamarche
7 July 2006
9:30–10:30 Max Schäfer
10:30–11:15 Ozan Kahramanogullari
- Talk about `Deepest of the Deep Inference´: The deep inference feature of the calculus of structures causes greater nondeterminism in proof search while providing shorter proofs than in the sequent calculus. We have seen that, by means of conditions that exploit an interaction schema on the structures, deep inference rules can be redesigned in such a way that reduces nondeterminism without losing the shorter proofs. However, when these interaction rules are applied during proof search to structures of arbitrary size, performing the check of the condition (resembling occurs-check of Prolog interpreters) of the interaction rules becomes computationally expensive. In this talk, we will present a general conjecture on the completeness of the calculus of structures systems where inference rules are allowed only at the `deepest´ positions. Because deepest instances of the inference rules are applied on the smaller substructures, the check of the condition of the interaction rules is performed only on these smaller structures.
11:15–12:15 Mark Price
- An introduction to logical frameworks providing motivation for future research.
12:15–13:00 Birgit Elbl
- Talk about `On Structural Detours in W-Style Proofs´.
14:30–15:15 Stéphane Lengrand
- Talk on higher-order type systems.
15:15–16:00 Lutz Straßburger
- Discussion on a `counter-example´ with some implications on the medial-switch-interaction fragment of SKS and the `splitting theorem´ (it also says that the category of derivations is not *-autonomous).
16:00–17:00 François Lamarche
- A tutorial about that denotational semantics for classical logic that I concocted a few months ago. This can also include the `categorical´ stuff, in which Lutz is also involved.
8 July 2006
11:00–12:30 François Lamarche
- A proposal for beating bureaucracies A and B simultaneously (the distinction actually disappears) using labeled posets. It seems very promising when we restrict ourselves to theories without equations and left-right-linear rewriting rules: in this particular case the gluing that replaces substitutions produces the required equalities completely naturally.
- This is an offshoot of my work on the homotopy (and directed homotopy) of posets and categories, which I presented in Montpellier in mid-May. The main point is that a poset or a category should directly be seen as a space, and that the standard geometric realization for its nerve is just another space, that has roughly but not exactly the same shape.
The meeting then moved to the lawns by the pond, where several football and verbal matches took place.
Locations
The initial meeting is on 6.7.06 at 9:30 in room 3E 4.17.
The following rooms are reserved:
- Thursday 6.7.06: room 3E 4.17 from 9:15 to 20:05
- Friday 7.7.06: room 1E 3.6 from 9:15 to 20:05
- Saturday 8.7.06: room 1E 3.6 from 9:15 to 20:05
The rooms are equipped with overhead projector and whiteboard, and a computer projector on request.
It's not straightforward to find the rooms, you need a campus map, and I suggest you access the campus from the main entrance, the stairway north of 4E; this gives access to the parade, from which you can access all the buildings, at their second level (the rooms I reserved are on the fourth and third level).
Instructions on how to get to the University of Bath.
Suggested accommodation: here.
Bath is a city full of interesting people.
16.7.2006 Alessio Guglielmi email
