| | | Module LI : Logique et mécanisation de l'inférence |
N.B.
Ce module est commun aux parcours FTI et IA.
Ce cours se compose de trois parties. Nous abordons d'abord les principaux résultats de logique classique, spécialement dans ses rapports à l'informatique: indécidabilité, complétude (semi-décidabilité) et incomplétude (de l'arithmétique). Les conséquences sur le pouvoir d'expression sont analysées. Une incursion dans l'ordre supérieur montre comment l'augmentation du pouvoir d'expression se fait au déficit de la complétude. Cette partie du cours s'appuie sur un document écrit d'une trentaine de pages, avec exercices.
On aborde ensuite les logiques non-classiques, illustrées par les logiques modales, permettant une expression plus fine de certaines notions (connaissance, prouvabilité, devoir, etc.) Cette partie permet d'introduire la sémantique des mondes possibles et ses rapports a l'axiomatique. Cette partie du cours s'appuie sur un document écrit d'une trentaine de pages, avec exercices.
Enfin, comme l'utilisation d'une logique et d'une axiomatique adéquate n'est pas suffisante pour en envisager la mécanisation, il faut encore introduire les notions et techniques indispensables a une mise en oeuvre pratique: certains systèmes de preuve comme la résolution et la méthode des tableaux, les stratégies et leurs propriétés, les classes décidables.
| | | Module LI : Logique et mécanisation de l'inférence |