Programmé en UV2 MAJ INF
Présentation :
La logique et la théorie des langages font partie des fondements de l'informatique. Dans ce module nous allons aborder certaines notions de ces théories.
Un langage est un ensemble de «mots» définis sur un «alphabet». Les expressions régulières (que l'on retrouve dans tous les langages de programmation modernes) sont un moyen de définir une classe particulière de langages, appelés langages réguliers. Les automates en donnent une description analytique (un mot appartient à un langage s'il peut être obtenu par une suite de transitions entre états de l'automate) et les grammaires formelles une description générative (un mot appartient à un langage s'il peut être obtenu par une suite de productions à partir d'un axiome de départ).
La logique étudie les principes du raisonnement. Dans ce cours, nous allons nous restreindre à la logique des prédicats (tout en considérant la logique propositionnelle en tant que cas particulier).
La logique des prédicats ou logique de premier ordre est une formalisation du langage des mathématiques. Elle utilise des fonctions, des variables, des prédicats, des connecteurs et des quantificateurs, assemblés en énoncés. Grâce à l'inférence on peut raisonner, c'est-à-dire obtenir de nouveaux énoncés à partir d'énoncés donnés. Ces opérations sont purement syntaxiques. L'utilité de la logique provient du fait que les énoncés peuvent être interprétés. Une interprétation est l'application d'un énoncé dans un domaine donné (qui peut faire partie des mathématiques ou du monde réel) et a alors une valeur de vérité. Une interprétation pour laquelle un énoncé est vrai est appelée un modèle de celui-ci. Ainsi, par le biais des modèles, les raisonnements logiques s'appliquent à des problèmes du monde réel.
En guise d'application de cette partie du cours on s'intéressera à la formalisation et preuve de programmes informatiques.
Objectifs pédagogiques :
- Comprendre les notions d'automate, de langage formel, d'expression régulière, de grammaire formelle
- Utiliser les expressions régulières dans plusieurs contextes
- Démontrer des propositions logiques
- Démontrer des formules de logique de premier ordre
- Insérer des assertions dans un programme et les vérifier
Volume horaire :
21h
Contenu détaillé :
C/TP-LF1 (3 h) : Langages formels, langages réguliers, expressions régulières
C/TP-LF2 (3 h) : Automates d'états finis
C/PC-LF3 (3h) : Grammaires formelles
Troisième cours (3 h) : Logique propositionnelle, connecteurs, tables de vérité, évaluation, satisfiabilité, conséquence, équivalence, distributivité, lois de de Morgan, formes normales (CNF/DNF), algorithme de Horn, résolution, complétude et compacité de la résolution
Quatrième cours (3 h) : Logique de premier ordre, sémantique, vocabulaires, exemples de structures (graphes, tables de sgbd, nombres), théories et modèles, théorie de preuve, preuves formelles, forme normale prenexe, skolémisation, théorie de Herbrand, résolution
Année 2016/2017
Dernière mise à jour le 08-FEB-16
Validation par le responsable de programme le
|
