Objectifs (en termes de compétences)

- Comprendre et maîtriser les fondemants mathématiques d'un grand nombre de concepts et techniques des systèmes informatiques.

- Etre capable d'établir les liens entre ces fondements et différents domaines d'application (algorithmique, structures de données, intelligence artificielle, génie logiciel, bases de données, robotique, etc.).

- Etre capable de suivre une démarche rigoureuse pour formaliser des structures informatiques courantes et appliquer des raisonnements sur ces structures.

Objet de l'activité (principaux thèmes à aborder)

- Introduction à la logique mathématique: logique des propositions, logique des prédicats; théories du premier ordre.

- Mécanismes de raisonnement: résolution, réécriture, induction sur un ensemble bien fondé.

- Structures discrètes vue comme théories du premier ordre: égalité, ordres partiels, treillis; naturels, chaînes, arbres, listes, ensembles, multi-ensembles, tuples, etc.

Résumé : Contenu et Méthodes

- Préliminaires: ensembles, relations et fonctions, systèmes formels.

- Logique mathématique: (1) calcul des propositions - syntaxe, sémantique, règles d'inférence; (2) calcul des prédicats du premier ordre - syntaxe, sémantique, règles d'inférence, réfutation; (3) notion de théorie, modèles, consistance, inclusion et extension de théories.

- Théories équationnelles: théorie de l'égalité, théorie des ordres partiels, théorie des treillis, théorie des groupes.

- Théories inductives: relation biens fondées; induction générale sur un ensemble bien fondé; étude de quelques théories inductives de base - entiers, chaînes, arbres, listes, ensembles, multi-ensembles, tuples. Notion de générateur de structure, construction systématique d'axiomatisations, et démonstrations inductives de propriétés selon différents principes d'induction (récurrence, induction complète, etc.).

Illustrations élémentaires dans différents champs d'application: preuves de programmes, spécification de types abstraits, automatisation du raisonnement déductif, systèmes experts, robotique, bases de données, analyse syntaxique, etc.

Mise en oeuvre à l'aide de langages de programmation " déclaratifs " tels que PROLOG ou ML.

Autres informations (Pré-requis, Evaluation, Support, ...)

- Les séances de travaux pratiques hebdomadaires requièrent une participation active et la prépartion de questions/réponses et résolution, par petits groupes, de problèmes remis à la séance précédente. Plusieurs tests sont organisés au cours du quadrimestre de manière à contrôler le travail régulier de l'étudiant.

- Prérequis:
Maîtrise des mathématiques élémentaires (supposée acquise à l'issue des deux premières années de baccalauréat).

- Références :
(1) Syllabus en vente au SICI.

(2) Z. Manna and R. Waldinger, The Deductive Foundations of Computer Programming, Addison-Wesley, 1993.

(3) D. Gries, F. Schneider, A Logical Approach to Discrete Mathematics, Springer-Verlag, 1994.

- Modalités d'évaluation
Tests au cours du quadrimestre, et examen écrit en session.