Logique (INFO501_INFO)
Présentation
Introduction à la logique du premier ordre et ses applications en informatique (modélisation, satisfaction de contraintes, satisfiabilité, preuve de programmes)
Les TP permettront d’explorer différentes applications mentionnées en cours : implémentation partielle (en Python) et utilisation d’un SAT solveur, utilisation d’un assistant de preuves (Coq), introduction à Prolog.
Heures d'enseignement
| Cours Magistral | 6h | |
| Travaux Dirigés | 9h | |
| Travaux Pratiques | 12h |
Pré-requis obligatoires
Mathématiques de L1
Plan du cours
1 – logique propositionnelle : syntaxe des formules, sémantique (tables de vérités et algèbres de Boole), modélisation de contraintes et problème de satisfiabilité, SAT solveur et algorithme DPLL, démonstrations (déduction naturelle), correction et complétude
2 – logique du premier ordre : syntaxe des termes, formules et quantificateurs, substitutions et renomage, résolution, algorithme d’unification de Martelli et Montanari, Prolog, sémantique, notion de modèle, démonstrations (déduction naturelle), théorème de complétude, exemple : arithmétique, théorème d’incomplétude
Contacts
