En logique mathématique, la règle de résolution ou principe de résolution de Robinson est une règle d'inférence logique qui généralise le modus ponens. Cette règle est principalement utilisée dans les systèmes de preuve automatiques, elle est à la base du langage de programmation logique Prolog. La règle du modus ponens s'écrit et se lit : de p et de "p implique q", je déduis q. On peut réécrire l'implication "p implique q" comme "p est faux ou q est vraie". Ainsi, la règle du modus ponens s'écrit . La règle de résolution, elle, généralise la règle du modus ponens car elle s'applique sur des clauses quelconques. Une clause est une formule qui est une disjonction (un "ou") de littéraux (une proposition atomique ou une proposition atomique précédée d'une négation). Par exemple est une clause avec deux littéraux ("non p" et "q"). Ainsi, en logique propositionnelle, la règle de résolution s'écrit : Autrement dit, étant donné deux clauses et , on en déduit . La formule déduite, c'est-à-dire est appelé résolvant de et . Bien sûr, l'application de la règle est donnée à permutation près des littéraux. Par exemple : où dénote la contradiction (clause vide). En logique des prédicats les formules atomiques sont de la forme où est un symbole de prédicat et les sont des termes composés de constantes, de variables et de symboles de fonctions. La règle de résolution en logique des prédicats est similaire à la règle de résolution en logique propositionnelle mais les formules atomiques partagées par deux clauses ne doivent pas être identiques mais unifiables. Deux formules atomiques sont unifiables s'il existe une substitution des variables par des termes qui rend les deux formules identiques (voir unification). Par exemple : est une application de la règle de résolution en logique des prédicats. Elle se lit : de "P(a)" et de "(pour tout x) non P(x) ou Q(x)", je déduis "Q(a)". Ici, la formule atomique et la formule atomique sont unifiables avec la substitution . Plus généralement, la règle de résolution en logique des prédicats est : où est un unificateur principal des formules atomiques et .