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.
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.
Logic in CoQ.
Induction and co-induction.
|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|
Strada le Grazie 15
VAT number 01541040232
Italian Fiscal Code 93009870234
© 2020 | Verona University | Credits