First cycle
degree courses
Second cycle
degree courses
Single cycle
degree courses
School of Science
COMPUTER SCIENCE
Course unit
LOGIC 2
SC02111834, A.A. 2015/16

Information concerning the students who enrolled in A.Y. 2015/16

Information on the course unit
Degree course Second cycle degree in
COMPUTER SCIENCE
SC1176, Degree course structure A.Y. 2014/15, A.Y. 2015/16
N0
bring this page
with you
Number of ECTS credits allocated 6.0
Type of assessment Mark
Course unit English denomination LOGIC 2
Website of the academic structure http://informatica.scienze.unipd.it/2015/laurea_magistrale
Department of reference Department of Mathematics
Mandatory attendance No
Language of instruction Italian
Branch PADOVA
Single Course unit The Course unit can be attended under the option Single Course unit attendance
Optional Course unit The Course unit can be chosen as Optional Course unit

Lecturers
Teacher in charge MARIA EMILIA MAIETTI MAT/01

Mutuating
Course unit code Course unit name Teacher in charge Degree course code
SC03119738 MATHEMATICAL LOGIC 2 MARIA EMILIA MAIETTI SC1172

ECTS: details
Type Scientific-Disciplinary Sector Credits allocated
Educational activities in elective or integrative disciplines MAT/01 Mathematical Logic 6.0

Course unit organization
Period First semester
Year 1st Year
Teaching method frontal

Type of hours Credits Teaching
hours
Hours of
Individual study
Shifts
Practice 2.0 16 34.0 No turn
Lecture 4.0 32 68.0 No turn

Calendar
Start of activities 01/10/2015
End of activities 28/01/2016
Show course schedule 2019/20 Reg.2014 course timetable

Examination board
Board From To Members of the board
8 Logica Matematica 2 - a.a. 2019/2020 01/10/2019 30/09/2020 MASCHIO SAMUELE (Presidente)
MAIETTI MARIA EMILIA (Membro Effettivo)
BONOTTO CINZIA (Supplente)
CIRAULO FRANCESCO (Supplente)
7 Logica Matematica 2 - a.a. 20182019 01/10/2018 30/09/2019 MASCHIO SAMUELE (Presidente)
MAIETTI MARIA EMILIA (Membro Effettivo)
BONOTTO CINZIA (Supplente)
CIRAULO FRANCESCO (Supplente)
SAMBIN GIOVANNI (Supplente)
6 Logica Matematica 2 - 2017/2018 01/10/2017 30/09/2018 SAMBIN GIOVANNI (Presidente)
MAIETTI MARIA EMILIA (Membro Effettivo)
CIRAULO FRANCESCO (Supplente)
MASCHIO SAMUELE (Supplente)
5 Logica Matematica 2 - 2016/2017 01/10/2016 30/11/2017 SAMBIN GIOVANNI (Presidente)
MAIETTI MARIA EMILIA (Membro Effettivo)
BONOTTO CINZIA (Supplente)
CIRAULO FRANCESCO (Supplente)
MASCHIO SAMUELE (Supplente)
4 Logica Matematica 2 - a.a. 2015/2016 01/10/2015 30/09/2016 MAIETTI MARIA EMILIA (Presidente)
VALENTINI SILVIO (Membro Effettivo)
BONOTTO CINZIA (Supplente)
CIRAULO FRANCESCO (Supplente)
ZANARDO ALBERTO (Supplente)

Syllabus
Prerequisites: It is recommended to have followed an introductory course on logic
but it is not strictly necessary.
Target skills and knowledge: Expressive power and theoretical limits of the concept of formal proof.
Differences between classical and constructive reasoning.
Introduction to proof theory of constructive logic and mathematics and their applications to computer science.
Examination methods: The final examination will be chosen by the student among one of the following options:
1. oral examination about all the topics in the course;
2. written examination about all the topics in the course;
3. oral talk on a topic agreed with the teacher and deeply investigated by the student together with the presentation of solutions regarding exercises delivered by the teacher during the course.
Assessment criteria: The student is required to master the concepts presented in the course by himself/herself.
The student is required to solve some easy exercises to test his
understanding of the grasped concepts and its main properties.
Course unit contents: Sequent calculus for classical predicate logic.
Sequent calculus for intuitionistic predicate logic.
Decision procedure for propositional intuitionistic logic.
Constructive proof of Gentzen's cut elimination theorems for both calculi.
Peano arithmetics.
Heyting arithmetics.
Differences between Peano and Heyting arithmetics with respect to formal Church thesis and axiom of choice.
Sketches of proofs about Goedel incompleteness theorems and comparison between proofs for classical and constructive arithmetics.
Realizability (computational) semantics for Heyting arithmetics.
Brief sketched connection between the topics of proof-theory studied before and concepts of category theory and categorical logic.
Planned learning activities and teaching methods: The student is required to participate to the lectures actively,
to develop its critical sense together with grasping new notions.
Lectures will be followed by class discussions, exercises to be solved by the students alone and talks given on deep investigations
agreed with the teacher about topics delivered during the course.
Additional notes about suggested reading: Syllabus, class exercises, papers for deep investigations provided by the teacher.
Textbooks (and optional supplementary readings)
  • A. S. Troelstra and D. van Dalen, Constructivism in Mathematics. An Introduction. --: North-Holland, 1988. volume I and II Cerca nel catalogo
  • A. M. Pitts, Categorical Logic in Handbook of Logic in Computer Science, vol. 5. Algebraic and Logical Structures.. --: Oxford University Press, 2000. Chapter 2 Cerca nel catalogo
  • A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory. --: Cambridge University Press, 2000. second edition Cerca nel catalogo