Selected Topics in Proof Theory (Seminar)

1References

Course notes and research papers for the preparation of your talks will be provided in due time: see the lecture schedule.

Knowledge of some of the topics presented for course Structural Proof Theory and Abstract Logic Programming may be an advantage.

Most of the material, references, and general introduction are available at the Deep inference web site

2News

Mo 23/5/11 DS2: meeting, to recover one lost session on15/5 and prepare the schedule of your talks
Nothing scheduled on Friday 27 to let you prepare the talks.

3Course Info

The course will be structured as follow. I will first introduce in form of lectures the methodology of deep inference, its motivations, the p[roblems it intends to address, some techniques proper of the methodology. Some of the concepts or toipics that will be presented can constitute the theme for students to prepare a seminar. The sooner we complete the introductory, lecturing part, the more will be the time for the students for prepare their presentation. It is crucial that all students taking part to the seminar attend all presentations of their fellows.

Lectures and topics

15.04.11—Lecture 1Presentation of the course, structure of the course/seminar, motivations to introduce deep inference.

29.04.11—Lecture 2 and 3Calculus of structures: terminology, basic definitions, dualities in systems. Classical logic: system SKSg and SKS. Correspondence with sequent calculus. Cut elimination procedure. General discussion on possible topics for seminars.

• Refer to the deep inference web site for general information.
• List of proposed topics for seminars (with the starting, minimal, reference point):
  

1. The need for Deep Inference (references: Alwen Tiu's paper and you may find some useful pictures from his thesis)
   
2. BV is NP-complete (reference)
   
3. Proof complexity in deep inference (reference)
   
4. Modal logic in deep inference (reference)
   
5. Technique of splitting in the calculus of structures (reference)
   
6. Multiplicative Exponential Linear Logic in deep inference (reference)
   
7. ... (more topics if needed)

6.05.11—Lecture 4 Proof complexity in the calculus of structures (for propositional classical logic)

23.05.11—Lecture 5 The idea of the splitting theorems for cut-elimination.

4Tutors and Office Hours

I don't have tutors. The Open House slot is a good venue to discuss your questions, or please just drop me an email and we'll arrange for an appointment.

6.6.11Paola Bruscoliemail (replace AT by @)