-
Arithmétique de Peano, 1.4.2
- Axiomes, 1.4.1
- Base de Herbrand, 2.4.2
- Clauses de Horn, 4.3.3
- Formule close, 1.2.3
- Terme clos, 1.2.3
- Conjonction élémentaire, 3.1.3
- Conséquence logique, 2.3
- clause, 3.1.2
- Définition récursive sur les termes, 1.5.3
- Domaine de Herbrand, 2.4.2
- Environnement, 2.1.3
- Equivalence, 2.3
- Forme clausale, 3.1.3, 3.1.4
- Forme normale de négation, 2.3.2
- Forme normale disjonctive, 3.1.3, 3.1.3
- Forme prénexe, 3.1.4
- Formule
- Formule atomique, 1.1.2
- Formule universelle, 2.4.2
- filtrage, 4.2.3
- Herbrand
-
Base de Herbrand, 2.4.2
- Domaine de Herbrand, 2.4.2
- Interprétation de Herbrand, 2.4.2
- Modèle de Herbrand, 2.4.2
- Insatisfiable (formule), 1.3.1
- Instance close, 2.4.2
- Interprétation, 2.1.1
- Interprétation de Herbrand, 2.4.2
| - littéral, 3.1.1
- Modèle d’une théorie, 1.4.1
- Modèle de Herbrand, 2.4.2
- motif, 4.2.3
- Preuve par résolution, 4.3.1
- Réfutation par résolution, 4.3.1
- Résolution
-
Déduction par résolution, 4.3.2
- Règles de résolution, 4.3.2
- Résolution propositionnelle
-
Déduction par résolution, 4.3.1
- Règle de résolution, 4.3.1
- Satisfiable (formule), 1.3.1
- Signature, 1.1.1, 1.4.1
- Substitution, 1.5.3
-
Substitution (terme), 1.5.3
- Substitution (formule), 1.2.3, 1.5.3
- Table de vérité, 1.3.1
- Tautologie, 1.3.1
- Terme, 1.1.1
- Théorie, 1.4.1
- Théorie de l’égalité, 1.4.2
- Unificateur, 4.2.1
- Unificateur principal, 4.2.2
- Unification, 4.2.2
- Valide (formule), 1.3.1
- Variables liées, 1.2.3
- Variables libres, 1.2.3
|
