Algoritmo de Wang

O algoritmo de Wang é um algoritmo desenvolvido por Hao Wang que testa se dadas conclusões são consequência lógica de determinadas premissas. Em lógica proposicional, pode-se dizer que é uma simplificação do método dos tablôs analíticos.

Algoritmo

Uma dedução natural qualquer pode ser escrita como:

$a_{1},a_{2},\cdots ,a_{3}\vDash b_{1},b_{2},\cdots ,b_{n}$

Numa dedução natural, toda a vez que as premissas forem simultaneamente verdadeiras, as conclusões também devem ser. Afirmam-se as premissas como verdadeiras, e as conclusões como falsas: se dessa forma obtiverem-se contradições em todas as "colunas" do desenvolvimento, a dedução é válida. Uma única coluna em que não haja contradição torna a dedução inválida.

$\left(a_{1},a_{2},\cdots ,a_{3}\right)\ \left(b_{1},b_{2},\cdots ,b_{n}\right)$

Nessa notação, os parênteses à esquerda representam fórmulas verdadeiras e os da esquerda, falsas. A partir daí, há algumas regras de desenvolvimento, que podem ser do tipo α ou β. As fórmulas devem conter apenas os operadores ∧, ∨ e ¬.

Fórmulas tipo "alfa"

São fórmulas que têm única solução possível. Ou seja, a partir da informação a respeito de uma fórmula ser válida ou não, pode-se chegar a uma única conclusão.

Se diz-se que ¬a é uma fórmula verdadeira, então a é falso.

${\begin{matrix}\left(\cdots ,\neg a,\cdots \right)\ \left(\cdots \right)\\\vdots \ _{\alpha \neg }\\\left(\cdots \right)\ \left(\cdots ,a,\cdots \right)\end{matrix}}$

Se diz-se que ¬a é uma fórmula falsa, então a é verdadeiro.

${\begin{matrix}\left(\cdots \right)\ \left(\cdots ,\neg a,\cdots \right)\\\vdots \ _{\alpha \neg }\\\left(\cdots ,a,\cdots \right)\ \left(\cdots \right)\end{matrix}}$

Se diz-se que a ∧ b é uma fórmula verdadeira, então a e b são verdadeiros simultaneamente.

${\begin{matrix}\left(\cdots ,a\land b,\cdots \right)\ \left(\cdots \right)\\\vdots _{\alpha \land }\\\left(\cdots ,a,b,\cdots \right)\ \left(\cdots \right)\end{matrix}}$

Se diz-se que a ∨ b é uma fórmula falsa, então a e b são falsos simultaneamente.

${\begin{matrix}\left(\cdots \right)\ \left(\cdots ,a\lor b,\cdots \right)\\\vdots \ _{\alpha \lor }\\\left(\cdots \right)\ \left(\cdots ,a,b,\cdots \right)\end{matrix}}$

Fórmulas tipo "beta"

São fórmulas que têm duas soluções possíveis, que devem ser desenvolvidas à parte.

Se diz-se que a ∧ b é uma fórmula falsa, então ou a é falso ou b é falso.

${\begin{matrix}\left(\cdots \right)\ \left(\cdots ,a\land b,\cdots \right)\\{\begin{matrix}\vdots _{\beta \land 1}&&\vdots _{\beta \land 2}\\\left(\cdots \right)\ \left(\cdots ,a,\cdots \right)&&\left(\cdots \right)\ \left(\cdots ,b,\cdots \right)\end{matrix}}\end{matrix}}$

Se diz-se que a ∨ b é uma fórmula verdadeira, então ou a é verdadeiro ou b é verdadeiro.

${\begin{matrix}\left(\cdots ,a\lor b,\cdots \right)\ \left(\cdots \right)\\{\begin{matrix}\vdots _{\beta \lor 1}&&\vdots _{\beta \lor 2}\\\left(\cdots ,a,\cdots \right)\ \left(\cdots \right)&&\left(\cdots ,b,\cdots \right)\ \left(\cdots \right)\end{matrix}}\end{matrix}}$

Referências

• Monard, M.C., Nicoletti, M.C.: Método sintático de prova de teoremas: algoritmo de Wang.
• Wang, Hao: Toward Mechanical Mathematics.