suivant:
4. Logique du premier
monter:
Logique et démonstration automatique
précédent:
3. Déduction Naturelle
Table des matières
Index
II. Logique du premier ordre
Sous-sections
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.4.1 Sens des termes sur une signature
4.3.4.2 Sens des formules atomiques sur une signature
4.3.4.3 Sens des formules sur une signature
4.3.5 Modèle, validité, conséquence, équivalence
4.3.6 Instanciation
4.3.7 Interprétation finie
4.3.7.1 Les entiers et leurs représentations
4.3.7.2 Expansion d'une formule
4.3.7.3 Interprétation et assignation propositionnelle
4.3.7.4 Recherche d'un modèle fini d'une formule fermée
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.1.1 Transformation en formule normale
5.2.1.2 Transformation en formule propre
5.2.1.3 Élimination des quantificateurs existentiels
5.2.1.4 Transformation en fermeture universelle
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.3.2.1 Les règles de l'algorithme
5.3.2.2 Correction de l'algorithme
5.3.2.3 Terminaison de l'algorithme
5.4 Résolution au premier ordre
5.4.1 Trois règles pour la résolution
5.4.1.1 Factorisation
5.4.1.2 Copie d'une clause
5.4.1.3 Résolution binaire
5.4.1.4 Preuve par factorisation, copie et résolution binaire
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.1.1 Règles pour le quantificateur universel
6.1.1.2 Règles pour le quantificateur existentiel
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
Benjamin Wack 2013-01-08
