Técnicas dedutivas

O conceito de prova formal é fundamental para a construção de conhecimento em muitas áreas, principalmente nas ciências exatas. Desenvolver uma prova consiste em derivar de um conjunto de premissas, através das regras de inferência e leis de equivalência, uma proposição que seja uma consequência lógica das premissas.
Existem diversas formas de desenvolver uma prova para um argumento, cada uma tem as suas peculiaridades e se adequam melhor a determinadas situações.

Prova direta

Dado um conjunto de fórmulas ${\alpha }_1,{\alpha }_2,{\alpha }_3,\dots ,{\alpha }_{n-1}$ e ${\alpha }_n$, diz-se que uma sequência finita de fórmulas ${\beta }_1,{\beta }_2,\dots ,{\beta }_k$ é uma prova (ou dedução) de ${\alpha }_n$ a partir das premissas ${\alpha }_1,{\alpha }_2,{\alpha }_3,\dots ,{\alpha }_{n-1}$ se e somente se:

1. Cada ${\beta }_i$ for uma premissa $a_j(1\le j\le n-1)$; ou
2. Cada ${\beta }_i$ que não for uma premissa for derivada das fórmulas precedentes aplicando-se um conjunto de regras de inferência; ou
3. Cada ${\beta }_i$ que não for uma premissa for obtida pela substituição de uma fórmula anterior por outra logicamente equivalente; ou
4. ${\beta }_k$ é a própria ${\alpha }_n$.

Dessa forma, para provar que ${\alpha }_n$ é uma conclusão válida das premissas ${\alpha }_1,{\alpha }_2,\dots ,{\alpha }_{n-1}$, é necessário produzir uma sequência de demonstração de forma que as premissas sejam derivadas em proposições ${\beta }_1,{\beta }_2,\dots ,{\beta }_k$ até que se atinja a proposição ${\alpha }_n$, ou seja, até que ${\beta }_k\equiv {\alpha }_n$.

Prova condicional

A prova condicional segue a mesma base da prova direta, porém além das premissas e proposições derivadas, introduz-se uma ou mais premissas provisórias chamadas de hipóteses, é importante destacar que todas as hipóteses devem ser descartadas até o final da prova. Além disso, as hipóteses devem ser descartadas na ordem inversa em que foram introduzidas.
Para provar uma conclusão que tem a forma condicional, por exemplo $p⟹q$, a partir de um conjunto de premissas, deve-se introduzir o antecedente $p$ como uma hipótese, deduzir $q$ utilizando $p$ e, no final, descartar a hipótese $p$ reconstruindo $p⟹q$.

Esse método de prova é embasado no Teorema da dedução
Sejam $\delta$ e $\beta$ duas fórmulas bem-formadas (proposições válidas) e ${\alpha }_1,\dots ,{\alpha }_n$ um conjunto de premissas. Então, as proposições ${\alpha }_1,\dots ,{\alpha }_n$ e $\delta$ implicam logicamente $\beta$ se e somente se as proposições ${\alpha }_1,\dots ,{\alpha }_n$ implicarem logicamente $\delta ⟹\beta$, ou seja:

$${\alpha }_1,{\alpha }_2,{\alpha }_3,\dots ,{\alpha }_n,\delta \models \beta ⟺{\alpha }_1,{\alpha }_2,{\alpha }_3,\dots ,{\alpha }_n\models \delta ⟹\beta$$

Prova indireta (redução ao absurdo)

A prova indireta se baseia no princípio de que a partir de uma contradição pode-se deduzir qualquer proposição.

Para provar uma conclusão $\beta$ através de uma prova indireta, deve-se introduzir a negação $\neg \beta$ da conclusão no conjunto de premissas como uma hipótese e então deduzir uma contradição. Ao chegar na contradição, prova-se a validade do argumento.

Inferência por resolução

A inferência por resolução é um método simples e eficiente para inferir conclusões lógicas a partir de premissas. Ao contrário dos demais métodos de prova, esse não exige a aplicação direta de operações baseadas nas regras de inferência e leis de equivalência. Ao invés disso, a inferência por resolução se baseia na manipulação de fórmulas na forma normal, mais especificamente na forma normal conjuntiva (FNC).

Dadas duas cláusulas $\alpha$ e $\beta$ e um literal $p$ tal que $p\in \alpha$ e $\neg p\in \beta$. Então

$$\left\{\alpha ,\beta \right\}\models \text{resolvente}(\alpha ,\beta ;p)$$

Tal que

$$\text{resolvente}(\alpha ,\beta ;p)=(\alpha -p)\cup (\beta -p)$$

Ou seja, o $\text{resolvente}$ é a cláusula obtida pela união de $\alpha$ e $\beta$ removendo-se o literal $p$ e seu complementar de ambas as cláusulas.

O método de inferência por resolução é um método de inferência por refutação, ou seja, o objetivo é refutar a conclusão ou todo o teorema. Portanto, deve-se negar a conclusão (ou o teorema todo) e fazer sucessivas regras de resolução entre as cláusulas para eliminar os literais até chegar-se em uma cláusula vazia ($\text{nil}$ ).

Uma cláusula $\alpha$ pode ser inferida por resolução de um conjunto de cláusulas $\Gamma$ ($\Gamma {⊢}_{\text{RES}}\alpha$) se a partir do conjunto $\Gamma \cup \left\{\neg a\right\}$ obtém-se a cláusula vazia ($\text{nil}$).

É importante destacar que esse método de inferência só é aplicável à cláusulas, portanto é necessário antes de tudo transformar todas as fórmulas do argumento em cláusulas.