Informatique théorique

Il sera alors abordé dans ce cours les notions fondamentales sous-jacentes aux thèmes 

• de l'induction et la récurrence (ensemble bien-fondé et équivalence avec l'induction mathématique). L'objectif est de formaliser les notions fondamentales d'induction et récursivité sous-jacentes à toutes les mathématiques discrètes.

• de l'algorithmique (fonctions récursives de Gödel/Herbrand, machine de Turing et tous les résultats d’indécidabilité associés). L'idée est de définir formellement (i.e. mathématiquement) ce qu'est un problème de décision et donner une dénotation formelle à la notion d'algorithme (thèse de Church).

• de la logique (syntaxe, sémantique et systèmes de preuves). L’intérêt des logiques est d’exprimer de façon formelle les propriétés des systèmes et de raisonner, de façon automatique ou assistée, à propos de ces propriétés. Les logiques propositionnelles et du premier ordre seront détaillées.

Le cours est composé des parties suivantes :

• Fondements de l'induction et la récursivité.

On y abordera plus particulièrement les notions de : Théorie des ensembles : Ordre et préordre, Majorants et minorants, Ensembles bien fondés et induction; Systèmes formels, preuves, correction et complétude.

• Logique propositionnelle.

  La logique propositionnelle sera présentée selon les composantes classiques : syntaxe, sémantique et preuve. En particulier, les points suivants seront abordés : arbres binaires de décision, méthode des tableaux, algorithme DPLL, satisfiabilité des formules propositionnelles (problèmes SAT et 3-SAT), SAT-solveurs, les systèmes de preuve de la résolution, déduction naturelle, séquents.

• Théorie de la calculabilité et de la complexité.

On verra plus précisément : les fonctions primitives récursives, les fonctions récursives, les problèmes décidables, indécidabilité du problème de l'arrêt, fonction récursive universelle (interpréteur) ; les machines de Turing , théorèmes d'équivalence, thèse de Church ; la théorie de la complexité en lien avec les modèles de calcul (complexité en temps, classes P et NP, structuration de la classe NP - problèmes NP-complets et NP-durs, un premier problème NP-complet) ; la décidabibilité et NP-complétude du problème 3-SAT.

• Logique des prédicats

La logique des prédicats est une extension de la logique propositionnelle et est la logique privilégiée pour décrire les structures de données informatiques. On verra que la logique des prédicats est indécidable et la programmation logique sera introduite.