Modélisation logique et systèmes formels
Ref: 3IF1050
Description
Présentation des principes fondamentaux et des outils formels (i.e. mathématiquement fondés) à la base à la fois de toutes les méthodes de conception, de vérification et d’implantation des systèmes informatiques. Ainsi, il sera alors abordé dans ce cours les notions fondamentales de la logique mathématique et de la démonstration automatique à la base de toutes ces techniques de modélisation et de vérification de systèmes informatiques. Il sera ainsi présenté des formalismes logiques dits classiques tels que la logique du 1er ordre mais aussi non classiques tels que les logiques modales très utilisées dans la modélisation des systèmes multi-agents et la représentation des données.
Période(s) du cours
SD9
Syllabus
Dans ce cours seront abordés les points suivants :
1. Logique propositionnelle
1.1 Rappel syntaxe, sémantique et résultats de base (compacité, NP-complétude) 1.2 Calcul (à la Hilbert, séquent, méthode des tableaux)
2. Logique des prédicats
2.1 Syntaxe, sémantique et résultats de base (Herbrand, indécidabilité, Loweinem/Skolem,etc.)
2.2 Calcul (à la Hilbert et preuve de complétude, séquent et élimination des coupures, résolution)
2.3 TP/TD avec utilisation du système Coq.
3. Logique modale
3.1 Syntaxe, sémantique et résultats d base (théorème de modèle fini et décidabilité, bissimulation et co-induction, théorème de Van Benthem)
3.2 Calcul (à la Hilbert, séquent et méthodes des tableaux)
3.3 Modélisation des langages de flôts - automate de Mealy et mu-calcul
Composition du cours
Ce cours essentiellement théorique sera exclusivement constitué de cours magistraux et de pcs d’application. Il est prévu 1 séance de TP/TD avec utilisation du système de preuve Coq.
Ressources
Polycopié du cours en français + énoncés de pcs et leur correction.
Résultats de l'apprentissage couverts par le cours
Savoir modéliser et raisonner pour renforcer la qualité des systèmes.