Table of Contents
Fondements des systemes de preuves / Foundations of proof systems (24h, 3 ECTS)Responsable : Gilles Dowek LanguageThe course is in English. Teaching in 2021 - 2022ObjectivesThe topic of this course are the notions of formal proofs and of logical formalisms. The latter are considered through their possible implementation and use in proof systems (much as a programming language is implemented by a compiler). We present several formalisms, including type theories used in several proof systems such as Coq, Agda, HOL, Isabelle, PVS. A particular point of attention will be the articulation between reasoning and computation. When and where ?The lectures are on Tuesdays from 16:15 to 19:30, in the Sophie Germain Building, room 1002. First course Sept. 14th ScheduleSept 14th : Motivations, aim (good formalisms), First-Order Logic & Natural deduction, Deduction Modulo, Logical Cuts. slides (lecture 1) ExamFinal Exam, length 2 hours. Nov. 30th, 16:30 Prerequisites
InternshipsBibliographyPast examsTeam
|