Automated reasoning (2020/2021)

Course code
4S02796
Name of lecturer
Andrea Masini
Coordinator
Andrea Masini
Number of ECTS credits allocated
6
Academic sector
INF/01 - INFORMATICS
Language of instruction
Italian
Location
VERONA
Period
II semestre dal Mar 1, 2021 al Jun 11, 2021.

Lesson timetable

Go to lesson schedule

Learning outcomes

The aim of the course is to provide an introduction to the techniques of mechanization of logical reasoning, using tools based on automatic deduction systems or proof assistant systems. Particular importance will be given to the techniques of formalization and mechanical reasoning using goal-driven software systems. At the end of the course students will be able to deal with formalization and automatic verification using either automatic reasoners or proof-assistants. Students will be able to continue their studies in the field of mechanical reasoning, for example by developing master's theses.

Syllabus

Part 1- Foundations
Recalls of natural deduction (classical and intuitionistic)
Simple typed Lambda calculus.
Type checking and type inference.
The system F and the Calculus of Constructions.
Introduction to automatic deduction in propositional logic.
Part 2 - The Coq system
Simple proofs in Coq (Goal, assumptions and tactics).
Functional programming in CoQ.
Structured data types.
Polymorphism and higher order functions.
The tactics.
Logic in CoQ.
Induction and co-induction.

Reference books
Author Title Publisher Year ISBN Note
Bertot, Yves, Castéran, Pierre Interactive Theorem Proving and Program Development Springer-Verlag Berlin Heidelberg 2004 978-3-642-05880-6
Jean Louis Krivine, Rene Cori Lambda-calculus, Types and Models Ellis Horwood 1993 978-0130624079
van Dalen, Dirk Logic and Structure. (Edizione 5) Springer 2013 978-1-4471-4557-8

Assessment methods and criteria

Written examination