20410529 - LM510 - LOGICAL THEORIES 1

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

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 PAGE
https://sites.google.com/view/lm510/

Modalità Erogazione

LECTURES WITH EXERCISES in classroom and by streaming

Modalità Valutazione

questions and exercises on the topics covered in class with an individual seminar

scheda docente | materiale didattico

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 PAGE
https://sites.google.com/view/lm510/

Modalità Erogazione

LECTURES WITH EXERCISES in classroom and by streaming

Modalità Valutazione

questions and exercises on the topics covered in class with an individual seminar

scheda docente | materiale didattico

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 PAGE
https://sites.google.com/view/lm510/

Modalità Erogazione

LECTURES WITH EXERCISES in classroom and by streaming

Modalità Valutazione

questions and exercises on the topics covered in class with an individual seminar