Une méthode de preuve qui démontre l'insatisfiabilité d'un ensemble de clauses en appliquant de manière répétée la règle de résolution pour produire de nouvelles clauses jusqu'à dériver la clause vide, signe d'une contradiction.

Principe

Utiliser la règle binaire de résolution pour combiner des clauses contenant des littéraux complémentaires, éventuellement avec unification dans le cas du premier ordre, et contrôler la recherche (sélection, ordonnancement, subsomption) afin de rendre atteignable la dérivation de la clause vide si l'ensemble de clauses est insatisfiable.

Démonstration

À partir des clauses {p ∨ q, ¬q ∨ r, ¬r, ¬p}, résoudre p ∨ q avec ¬p pour dériver q, résoudre q avec ¬q ∨ r pour dériver r, résoudre r avec ¬r pour dériver la clause vide, réfutant ainsi l'ensemble initial.

Mauvaise application

Appliquer des procédures de résolution propositionnelle telles quelles à des ensembles de clauses du premier ordre sans unification ni stratégies de terminaison, ou supposer que la résolution produit toujours des preuves courtes ou lisibles ; une expansion naïve peut exploser combinatoirement.

Conséquence

La réfutation par résolution est correcte et, pour la logique propositionnelle et des réglages adaptés du premier ordre, complétement réfutante : si l'ensemble de clauses est insatisfiable, une réfutation existe ; elle sous-tend de nombreux prouveurs automatiques et solveurs SAT (après transformation en FNC et parfois avec des mécanismes supplémentaires).

Inversion

L'inversion est la recherche de preuve constructive (par exemple tableau ou déduction naturelle produisant une dérivation directe de la formule) au lieu de la réfutation par contradiction ; dans l'approche inversée on tente de construire un modèle ou une preuve directe plutôt que de dériver une contradiction.

Limite

Applicable aux représentations sous forme de clauses (FNC) ; la résolution pure ne construit pas en soi de modèles pour des ensembles satisfiables et, en logique du premier ordre, peut ne pas terminer sans stratégies ou restrictions appropriées (p. ex. ordonnancement, sélection ou contrôle de boucle).

Tension sémantique

Tension entre la réfutation par résolution et les styles de calculs de séquents ou de déduction naturelle : la résolution vise la réfutation et la recherche algorithmique sur les clauses, tandis que d'autres styles privilégient l'extraction constructive de témoins et des formes de preuve différentes.

Synthèse

La réfutation par résolution combine la règle d'inférence locale de résolution avec l'unification (en premier ordre) et le contrôle global de la recherche pour dériver des contradictions à partir d'ensembles de clauses ; elle transforme la tâche de prouver une validité en une recherche systématique d'élimination de clauses qui aboutit soit à la clause vide soit à l'échec de la réfutation.