Resolució (lògica)

En la lògica matemàtica i la demostració automatitzada de teoremes, la resolució és una regla d'inferència que condueix a una tècnica de demostració de teoremes de refutació completa per a oracions en lògica proposicional i lògica de primer ordre. Per a la lògica proposicional, l'aplicació sistemàtica de la regla de resolució actua com un procediment de decisió per a la insatisfabilitat de la fórmula, resolent el (complement del) problema de satisfacció booleà. Per a la lògica de primer ordre, la resolució es pot utilitzar com a base per a un semi-algoritme per al problema d'insatisfacció de la lògica de primer ordre, proporcionant un mètode més pràctic que un que segueix el teorema de completitud de Gödel.

La regla de resolució es remunta a Davis i Putnam (1960); tanmateix, el seu algorisme requeria provar totes les instàncies bàsiques de la fórmula donada. Aquesta font d'explosió combinatòria va ser eliminada l'any 1965 per l'algoritme d'unificació sintàctica de John Alan Robinson, que va permetre instanciar la fórmula durant la demostració "a demanda" tan lluny com era necessari per mantenir la refutació completa.

La clàusula produïda per una regla de resolució de vegades s'anomena resolutiva.

Resolució en lògica proposicional

Regla de resolució

La regla de resolució en lògica proposicional és una única regla d'inferència vàlida que produeix una nova clàusula implicada per dues clàusules que contenen literals complementaris. Un literal és una variable proposicional o la negació d'una variable proposicional. Es diu que dos literals són complements si un és la negació de l'altre (a continuació, $\lnot c$ es pren com a complement $c$ ). La clàusula resultant conté tots els literals que no tenen complements. Formalment:

${\frac {a_{1}\lor a_{2}\lor \cdots \lor c,\quad b_{1}\lor b_{2}\lor \cdots \lor \neg c}{a_{1}\lor a_{2}\lor \cdots \lor b_{1}\lor b_{2}\lor \cdots }}$

on

tots $a_{i}$, $b_{i}$, i $c$ són literals,

la línia divisòria significa " implica ".

L'anterior també es pot escriure com:

${\frac {(\neg a_{1}\land \neg a_{2}\land \cdots )\rightarrow c,\quad c\rightarrow (b_{1}\lor b_{2}\lor \cdots )}{(\neg a_{1}\land \neg a_{2}\land \cdots )\rightarrow (b_{1}\lor b_{2}\lor \cdots )}}$

O esquemàticament com:

${\frac {\Gamma _{1}\cup \left\{\ell \right\}\,\,\,\,\Gamma _{2}\cup \left\{{\overline {\ell }}\right\}}{\Gamma _{1}\cup \Gamma _{2}}}|\ell |$

Tenim la terminologia següent:

• Les clàusules $\Gamma _{1}\cup \left\{\ell \right\}$ i $\Gamma _{2}\cup \left\{{\overline {\ell }}\right\}$ són les premisses de la inferència
• $\Gamma _{1}\cup \Gamma _{2}$ (la resolució de les premisses) és la seva conclusió.
• El literal $\ell$ és l'esquerra resolta literalment,
• El literal ${\overline {\ell }}$ és el dret resolt literalment,
• $|\ell |$ és l'àtom o pivot resolt.

La clàusula produïda per la regla de resolució s'anomena resolució de les dues clàusules d'entrada. És el principi de consens aplicat a les clàusules més que als termes.

Quan les dues clàusules contenen més d'un parell de literals complementaris, la regla de resolució es pot aplicar (independentment) per a cada parell d'aquestes; tanmateix, el resultat és sempre una tautologia.

Modus ponens es pot veure com un cas especial de resolució (d'una clàusula d'un literal i d'una clàusula de dos literals).

${\frac {p\rightarrow q,\quad p}{q}}$

és equivalent a

${\frac {\lnot p\lor q,\quad p}{q}}$