Preuve automatique et preuves de programmes

FUNDP-INFO-3101 -- P.-Y. Schobbens -- 30-0-0 -- Cours de 3ème cycle

Objectif

On s'intéresse, ici, peu aux méthodes de preuves de programmes qui devraient faire l'objet d'un autre cours, mais plutôt aux techniques qui permettent l'implémentation des systemes de preuves.

Prérequis

• un minimum de preuve de programmes (p.ex. le système de Hoare);
• logique du premier ordre: syntaxe et modèles.
  ULB-INFO-362: Eléments de logique appliquée à l'informatique
  FUNDP-INFO-2209: Techniques d'Intelligence Artificielle

Contenu

1. Bases de théorie de la preuve : systèmes de Hilbert, déduction naturelle, séquents, élimination des coupures. Expression de preuve en lambda-calcul: isomorphisme de Curry-Howard, systèmes de types.
2. Bases de la preuve automatique :
   1. Algorithme de résolution, unification, unification d'ordre supérieur:
   2. Réécriture, paramodulation, surréduction.
3. Environnements interactifs d'aide à la preuve: HOL, Isabelle, KIV, PVS, B.

Pédagogie

Cours théorique + travaux avec un environnement interactif d'aide à la preuve

Références

1
J. H. Gallier, Logic for Computer Science: Foundations of Automatic Theorem Proving, Harper and Row, 1986.