University of Siena - Dipartimento di Ingegneria dell'Informazione e Scienze Matematiche
17, 18, 19, 20 , 24, 25, 26 Giugno ore 10-13.
Presso Pian dei Mantellini 44
Proof Theory is that part of mathematical logic which investigates the notion of
proof (deduction) in formal systems of logic. The course will deal with:
Natural Deduction and Sequent Calculus for classical and intuitionistic Logic.
Theorem of cut-elimination in sequent calculus and its consequences. The
typed Lambda calculus and the paradigm "proof-as-programs" known as Curry-Howard
isomorphism. Theorem of Church-Rosser and theorem of strong normalization (uniqueness
of result and termination for the proof-as-programs).