Logique

Cours

• Introduction, guide GIT
• Prolog, le côté algorithmique de la force
• Logique Propositionnelle
• Logique des prédicats
• Coq
• Logique intuitionniste
• SAT : Satisfaction booléenne
• Correspondance Curry-Howard
• Récursion primitive

Cours de Reynald Affeldt

• Le Raisonnement Logique dans l’Assistant de Preuve Coq

TD

• TD1 : introduction à Prolog
• TD2 : logique propositionnelle
• TD3 : logique propositionnelle
• TD4 : logique propositionnelle
• TD5 : logique du premier ordre
• TD6 : logique du premier ordre
• TD7 : SAT, DPLL et Récursion primitive

TP

Récupérez l'archive contenant les exercices à trous. Créez ensuite un projet sur le gitlab du FIL, et ajoutez la branche distante :

. Faites un commit après chaque question.

• TP1 : les listes
• TP2 : Sudoku
• TP3 : Coq
• TP4 : preuves et programmes en Coq

Interros

• Interro 1, 2015
• Interro 2, 2015
• Interro 3, 2015
• Interro 4, 2015
• Interro 5, 2015

Archives TP

• TP1 : introduction à Prolog
• TP4 : Interpréteur logique

Archives exams

• 2013 (anciennement AEL)
• 2013, session 2 (la moitié est sur les automates)
• 2015
• 2015, session 2

Lecture

• Page du cours de Coq de Reynald Affeldt
• Raymond Smullyan, Le livre qui rend fou
• René David, Karim Nour, Christophe Raffalli, Introduction à la logique