suivant:
1. Logique propositionnelle
monter:
Logique et démonstration automatique
précédent:
Introduction
Table des matières
Index
I. Logique propositionnelle
Sous-sections
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
2.3.5.1 Heuristique de branchement
2.3.5.2 Ajout de clauses
2.3.5.3 Analyse des conflits et retour-arrière non chronologique
2.3.5.4 Apprentissage
2.3.5.5 Redémarrage
2.3.5.6 Structures de données paresseuses
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.1.5.1 Brouillon de preuve
3.1.5.2 Contexte des lignes d'un brouillon de preuve
3.1.5.3 Preuves
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
Benjamin Wack 2013-01-08