Resolução
$$\Huge \ndResol $$
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 ($\ndResol$)
$$\Large \ndResol: ~\cbr{a \lor c, b \lor \neg c} \vdash a \lor b $$ ou $$\Large \ndrule{a \lor c & b \lor \neg c}{a \lor b}{\ndResol} $$
Exercício. Derive a regra da resolução das regras anteriores. Isto é, mostre que $$ \cbr{a \lor c, b \lor \neg c} \vdash a \lor b $$
A regra da resolução é mais útil na sua forma generalizada.
Resolução generalizada ($\ndResol$)
$$\large \ndrule{ a_1 \lor \cdots \lor a_N \lor \boxed{c_1 \lor \cdots \lor c_K} &\quad b_1 \lor \cdots \lor b_M \lor \boxed{\overline{c_1} \lor \cdots \lor \overline{c_K}} }{ a_1 \lor \cdots \lor a_N \lor b_1 \lor \cdots \lor b_M }{\ndResol} $$
No limite, quando $N = 0, M = 0$ obtemos $\cbr{c, \neg c} \vdash \bot$.
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 \vdash p$ com a regra da resolução:
- Convertem-se todas as proposições de $H$ e $\neg p$ para a forma normal conjuntiva.
- Verifica-se se $\cbr{H, \neg p} \vdash \alert{\bot}$ 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.