La résolution prouve qu'une formule n'a aucune solution, en combinant ses clauses deux à deux jusqu'à en produire une vide.
La règle
Deux clauses se résolvent quand l'une contient un littéral et l'autre sa négation. Le résolvant réunit tous les autres littéraux des deux clauses, ce littéral en moins.
Les clauses
| Clause | Contenu |
|---|---|
| C1 | a OU b |
| C2 | NON a OU c |
Objectif
Donner le résolvant de C1 et C2, en séparant les littéraux par OU, puis son nombre de littéraux.
Enfin, dire ce que donne la résolution de la clause (a) avec la clause (NON a). Répondre par vide s'il ne reste plus aucun littéral.