Table des matières

• I. Logique propositionnelle
  • 1. Logique propositionnelle
    • 1.1 Syntaxe
      • 1.1.1 Formules strictes
      • 1.1.2 Formules à priorité
    • 1.2 Sens des formules
      • 1.2.1 Sens des connecteurs
      • 1.2.2 Valeur d'une formule
      • 1.2.3 Définitions et notions élémentaires de logique
      • 1.2.4 Compacité
      • 1.2.5 Équivalences remarquables
    • 1.3 Substitution et remplacement
      • 1.3.1 Substitution
      • 1.3.2 Remplacement
    • 1.4 Formes Normales
      • 1.4.1 Transformation en forme normale
      • 1.4.2 Transformation en forme normale disjonctive (somme de monômes)
      • 1.4.3 Transformation en forme normale conjonctive (produit de clauses)
    • 1.5 Algèbre de Boole
      • 1.5.1 Définition et notations
      • 1.5.2 Propriétés
      • 1.5.3 Dualité
    • 1.6 Fonctions booléennes
      • 1.6.1 Fonctions booléennes et somme de monômes
      • 1.6.2 Fonctions booléennes et produit de clauses
    • 1.7 L'outil BDDC
  • 2. Résolution propositionnelle
    • 2.1 Résolution
      • 2.1.1 Définitions
      • 2.1.2 Cohérence
      • 2.1.3 Complétude pour la réfutation
      • 2.1.4 Réduction d'un ensemble de clauses
      • 2.1.5 Clauses minimales pour la déduction
      • 2.1.6 Clauses minimales pour la conséquence
    • 2.2 Stratégie complète
      • 2.2.1 Algorithme de la stratégie complète
      • 2.2.2 Arrêt de l'algorithme
      • 2.2.3 Le résultat de l'algorithme est équivalent à l'ensemble initial de clauses
      • 2.2.4 Le résultat de l'algorithme est l'ensemble des clauses minimales pour la déduction de l'ensemble initial de clauses
    • 2.3 Algorithme de Davis-Putnam-Logemann-Loveland
      • 2.3.1 Suppression des clauses contenant des littéraux isolés
      • 2.3.2 Résolution unitaire
      • 2.3.3 Suppression des clauses valides
      • 2.3.4 L'algorithme
      • 2.3.5 Solveurs SAT
  • 3. Déduction Naturelle
    • 3.1 Système formel de la déduction naturelle
      • 3.1.1 Règles de conjonction
      • 3.1.2 Règles de disjonction
      • 3.1.3 Règles de l'implication
      • 3.1.4 Deux règles spéciales
      • 3.1.5 Preuves en déduction naturelle
    • 3.2 Tactiques de preuve
    • 3.3 Cohérence de la déduction naturelle
    • 3.4 Complétude de la déduction naturelle
    • 3.5 Outils
      • 3.5.1 Logiciel de construction automatique de preuves
      • 3.5.2 Dessiner des arbres de preuves
  
  
• II. Logique du premier ordre
  • 4. Logique du premier ordre
    • 4.1 Syntaxe
      • 4.1.1 Formules strictes
      • 4.1.2 Formules à priorité
    • 4.2 Être libre ou lié
      • 4.2.1 Occurrences libres et liées
      • 4.2.2 Variables libres et liées
    • 4.3 Sens des formules
      • 4.3.1 Déclaration de symbole
      • 4.3.2 Signature
      • 4.3.3 Interprétation
      • 4.3.4 Sens des formules
      • 4.3.5 Modèle, validité, conséquence, équivalence
      • 4.3.6 Instanciation
      • 4.3.7 Interprétation finie
      • 4.3.8 Substitution et remplacement
    • 4.4 Équivalences remarquables
      • 4.4.1 Relation entre ∀ et ∃
      • 4.4.2 Déplacement des quantificateurs
      • 4.4.3 Changement de variables liées
  • 5. Base de la démonstration automatique
    • 5.1 Méthodes de Herbrand
      • 5.1.1 Domaine et base de Herbrand
      • 5.1.2 Interprétation de Herbrand
      • 5.1.3 Théorème de Herbrand
    • 5.2 Skolémisation
      • 5.2.1 Algorithme de skolémisation d'une formule
      • 5.2.2 Propriétés de la forme de Skolem
      • 5.2.3 Forme clausale
    • 5.3 Unification
      • 5.3.1 Unificateur
      • 5.3.2 Algorithme d'unification
    • 5.4 Résolution au premier ordre
      • 5.4.1 Trois règles pour la résolution
      • 5.4.2 Cohérence de la résolution
      • 5.4.3 Complétude de la résolution
  • 6. Déduction naturelle au premier ordre : quantificateurs, copie et égalité
    • 6.1 Règles pour la logique du premier ordre
      • 6.1.1 Règles des quantificateurs
      • 6.1.2 Copie
      • 6.1.3 Les règles de l'égalité
    • 6.2 Tactiques de preuves
      • 6.2.1 Raisonner en avant avec une hypothèse d'existence
      • 6.2.2 Raisonner en arrière pour généraliser
      • 6.2.3 Un exemple d'application des tactiques
    • 6.3 Cohérence du système
  
  
• Bibliographie
• Index