The course aims at giving basic knowledge of classical and some non-classical logics, their formal semantics and proof systems. Students will acquire the capability to use the studied logics for representation purposes and will be presented with some important applications of logic in computer science.
Curriculum
teacher profile teaching materials
M. Cialdea Mayer. Logica (lecture notes)
Any introductory book on Prolog.
SWI-Prolog user manual.
D. A. Peled. Software Reliability Methods. Springer, 2001 (chapters 1 and 4).
M. Cialdea Mayer. Logica temporale e verifica di proprietà dei programmi (lecture notes).
Programme
Classical first order logic (syntax and semantics). Automated proof methods. The resolution method, its refinements and SLD resolution. Logic programming and the Prolog language. Modal and temporal logics. The tableaux method for linear temporal logic. Application to system verification.Core Documentation
See the course web site: http://cialdea.dia.uniroma3.it/teaching/logica/M. Cialdea Mayer. Logica (lecture notes)
Any introductory book on Prolog.
SWI-Prolog user manual.
D. A. Peled. Software Reliability Methods. Springer, 2001 (chapters 1 and 4).
M. Cialdea Mayer. Logica temporale e verifica di proprietà dei programmi (lecture notes).
Type of delivery of the course
Live lessons and exercitationsType of evaluation
The written exam lasts approximately 2 hours. The exercises proposed aim at testing the students' understanding of the notions introduced in the course and their ability solve simple problems by using them. The texts of the exams of the last years can be found in the course web page: http://cialdea.dia.uniroma3.it/teaching/logica/. teacher profile teaching materials
M. Cialdea Mayer. Logica (lecture notes)
Any introductory book on Prolog.
SWI-Prolog user manual.
D. A. Peled. Software Reliability Methods. Springer, 2001 (chapters 1 and 4).
M. Cialdea Mayer. Logica temporale e verifica di proprietà dei programmi (lecture notes).
Mutuazione: 20810263 Logica in Ingegneria informatica LM-32 CIALDEA MARTA
Programme
Classical first order logic (syntax and semantics). Automated proof methods. The resolution method, its refinements and SLD resolution. Logic programming and the Prolog language. Modal and temporal logics. The tableaux method for linear temporal logic. Application to system verification.Core Documentation
See the course web site: http://cialdea.dia.uniroma3.it/teaching/logica/M. Cialdea Mayer. Logica (lecture notes)
Any introductory book on Prolog.
SWI-Prolog user manual.
D. A. Peled. Software Reliability Methods. Springer, 2001 (chapters 1 and 4).
M. Cialdea Mayer. Logica temporale e verifica di proprietà dei programmi (lecture notes).
Type of delivery of the course
Live lessons and exercitationsType of evaluation
The written exam lasts approximately 2 hours. The exercises proposed aim at testing the students' understanding of the notions introduced in the course and their ability solve simple problems by using them. The texts of the exams of the last years can be found in the course web page: http://cialdea.dia.uniroma3.it/teaching/logica/.