Address some questions of the theory of the proof of the twentieth century, in connection with the themes of contemporary research
Curriculum
scheda docente
materiale didattico
***************************************
Natural Deduction
Sequent Calculus for Classical Logic (LK) and Intuitionistic Logic (LJ)
Cut elimination for LK and LJ sequent proofs
Sequent calculus for Linear Logic(LL)
Cut Elimination Theorem for LL
Focusing Theorem for LL proofs
Proof Nets
*************************************
(proof-structures, correctness, normalization, adequacy, sequentialization, focusing, complexity)
Pure Multiplicative Proof Nets
Multiplicative and Additive Proof Nets
Multiplicative and Exponenial Proof Nets
https://sites.google.com/view/lm510/
Fruizione: 20710091 TEORIE LOGICHE 1 - LM in Scienze filosofiche LM-78 MAIELI ROBERTO
Programma
Sequent Calculus Proofs***************************************
Natural Deduction
Sequent Calculus for Classical Logic (LK) and Intuitionistic Logic (LJ)
Cut elimination for LK and LJ sequent proofs
Sequent calculus for Linear Logic(LL)
Cut Elimination Theorem for LL
Focusing Theorem for LL proofs
Proof Nets
*************************************
(proof-structures, correctness, normalization, adequacy, sequentialization, focusing, complexity)
Pure Multiplicative Proof Nets
Multiplicative and Additive Proof Nets
Multiplicative and Exponenial Proof Nets
Testi Adottati
Handbooks, papers, NOTES AND SLIDES AVAILABLE ON THE COURSE WEB PAGEhttps://sites.google.com/view/lm510/
Modalità Erogazione
LECTURES WITH EXERCISES in classroom and by streamingModalità Valutazione
questions and exercises on the topics covered in class with an individual seminar
scheda docente
materiale didattico
***************************************
Natural Deduction
Sequent Calculus for Classical Logic (LK) and Intuitionistic Logic (LJ)
Cut elimination for LK and LJ sequent proofs
Sequent calculus for Linear Logic(LL)
Cut Elimination Theorem for LL
Focusing Theorem for LL proofs
Proof Nets
*************************************
(proof-structures, correctness, normalization, adequacy, sequentialization, focusing, complexity)
Pure Multiplicative Proof Nets
Multiplicative and Additive Proof Nets
Multiplicative and Exponenial Proof Nets
https://sites.google.com/view/lm510/
Fruizione: 20710091 TEORIE LOGICHE 1 - LM in Scienze filosofiche LM-78 MAIELI ROBERTO
Programma
Sequent Calculus Proofs***************************************
Natural Deduction
Sequent Calculus for Classical Logic (LK) and Intuitionistic Logic (LJ)
Cut elimination for LK and LJ sequent proofs
Sequent calculus for Linear Logic(LL)
Cut Elimination Theorem for LL
Focusing Theorem for LL proofs
Proof Nets
*************************************
(proof-structures, correctness, normalization, adequacy, sequentialization, focusing, complexity)
Pure Multiplicative Proof Nets
Multiplicative and Additive Proof Nets
Multiplicative and Exponenial Proof Nets
Testi Adottati
Handbooks, papers, NOTES AND SLIDES AVAILABLE ON THE COURSE WEB PAGEhttps://sites.google.com/view/lm510/
Modalità Erogazione
LECTURES WITH EXERCISES in classroom and by streamingModalità Valutazione
questions and exercises on the topics covered in class with an individual seminar