Resolução

$$\mathbb{R}$$

One Ring to bring them all and in the darkness bind them

A Resolução é uma regra que substitui todas as outras e funciona associada à forma normal disjuntiva.

Resolução ($\mathbb{R}$)

$$\mathbb{R}:\left\{a\vee c,b\vee \neg c\right\}⊢a\vee b$$ ou $$\frac{\begin{array}{cc}a\vee c& b\vee \neg c\end{array}}{a\vee b}\left(\mathbb{R}\right)$$

Exercício. Derive a regra da resolução das regras anteriores. Isto é, mostre que $$\left\{a\vee c,b\vee \neg c\right\}⊢a\vee b$$

A regra da resolução é mais útil na sua forma generalizada.

Resolução generalizada ($\mathbb{R}$)

$$\frac{\begin{array}{cc}{a}_1\vee \cdots \vee a_N\vee \boxed{c_1\vee \cdots \vee c_K}& b_1\vee \cdots \vee b_M\vee \boxed{\overline{c_1}\vee \cdots \vee \overline{c_K}}\end{array}}{a_1\vee \cdots \vee a_N\vee b_1\vee \cdots \vee b_M}\left(\mathbb{R}\right)$$

No limite, quando $N=0,M=0$ obtemos $\left\{c,\neg c\right\}⊢\perp$.

Algoritmo de Resolução

Com as proposições escritas na FNC, a regra da resolução pode substituir todas as outras.

Para se verificar se $H⊢p$ com a regra da resolução:

1. Convertem-se todas as proposições de $H$ e $\neg p$ para a forma normal conjuntiva.
2. Verifica-se se $\left\{H,\neg p\right\}⊢\perp$ por aplicações sucessivas da resolução.

(Mais tarde, na secção "Exemplos" o algoritmo da resolução é aplicado a alguns problemas.)

O algoritmo de resolução, juntamente com a unificação, é a base da linguagem lógica Prolog.