UAF501 Outils formels

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.

Mathématiques de L1

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