Notice: Undefined offset: 0 in /home/web/Documents/OrgNew/includes/header.inc.php on line 22
ICCL

About  |  Study  |  Members  |  Projects  |  Publications  |  Events  |  Search  |  Internals  |  Contact & Imprint

Courses in Winter Term 2007/08  -  Introduction to Deep Inference and Proof Nets


Course title:  Introduction to Deep Inference and Proof Nets

Lecturer:   Dr. Paola Bruscoli, Dr. Lutz Strassburger

Module:  IT

Status:  advanced unit

SWS (lecture/tutorial/practical):  1/0/0

Credit points:  1

Examination method:  written examination

Prerequisites:  aquaintance with the basics of propositional classical logic

Course description:

The course is intended to be an introduction into the venerable field of proof theory via the novel concepts of deep inference and proof nets. Deep inference can be understood as a principle for designing a deductive system for a logic. It is based on the idea of rewriting a formula inside arbitrary contexts, which is alien to other formalisms like sequent calculus. On the other hand, proof nets are a graph like presentation of formal proofs. The basic idea is to abstract away from unrelevant syntactic "bureaucracy" that is usually involved in deductive systems. Deep inference and proof nets do not solely give new insights into traditional results of proof theory, like cut elimination, rather they overcome traditional methodologies in at least the following respects:

  1. New normal forms and decomposition theorems, available thanks to deep inference, provide a richer proof theory;
  2. Some logics, motivated by modern computer science, that cannot be treated in traditional proof theoretical methodologies, find in deep inference a natural setting for being studied.

References

Additional Information: