|
Courses and Workshops
|
| Title: | The calculus of structures |
| Lecturer(s): | Alessio Guglielmi (Technische Universitaet Dresden) |
| Type: | Advanced Course |
| Section: | Logic and Computation |
| Week: | Second | | Time: | 9.00-10.30 (Slot 1) |
| Webpage: | http://alessio.guglielmi.name/
|
| Reader: | Download | | Room: | C1 |
Description The Calculus of Structures is a proof-theoretical formalism motivated by
computation. Its most direct analogue is Gentzen's Sequent Calculus.
We know that systems in the Sequent Calculus can be interpreted
computationally, in the proof-normalisation-as-computation and
proof-search-as-computation paradigms. Many aspects of computation are
not managed satisfactorily by the Sequent Calculus, especially some
important for distributed computation, like locality, atomicity and
several kinds of modularity. This holds for all logics expressed in the
Sequent Calculus, including, e.g., Linear Logic.
The Calculus of Structures addresses these problems in a radically new,
purely proof-theoretical foundation, based on the principles of deep
inference and top-down symmetry. We express classical, linear, modal
logics, and several variants thereof, and their deductive systems are as
simple as those in the Sequent Calculus, but possess the desired
computational properties. This new proof theory is richer than the old
one, e.g., there are new interesting notions of normalisation.
/Further particulars/
Absolute prerequisite: Sequent Calculus; it would be very desirable to
know about natural deduction and cut elimination; knowing some linear
logic might be helpful but not essential.
Web page with all the details about the Calculus of Structures, papers,
frequently asked questions etc.:
http://alessio.guglielmi.name/res/cos
Mailing list about the Calculus of Structures:
http://alessio.guglielmi.name/frogs
|
© 2003, 2004 LORIA, Carlos Areces. |
2004-04-20
| |
