Verifique a validade dos argumentos, usando tableaux semânticos ou resolução
,
Passo 1
O enunciado pede para verificar se, a partir das premissas
,
,
e
, podemos deduzir
. O conteúdo aqui é lógica proposicional e a técnica que vamos usar é o método de resolução, que mostra que não é possível as premissas serem todas verdadeiras enquanto a conclusão é falsa.
Passo 2
No método de resolução a gente reúne todas as premissas em forma de cláusulas na Forma Normal Conjuntiva (CNF) e ainda inclui a negação da conclusão (aqui
). Se a partir desse conjunto conseguirmos derivar a cláusula vazia (contradição), então as premissas implicam a conclusão.
Passo 3
Convertendo cada fórmula para CNF e numerando as cláusulas, temos:
Passo 4
Agora aplicamos a resolução entre pares de cláusulas:
Pelo par e
, resolvendo em cima de
, obtemos
Pelo par
Passo 5
Em seguida, resolvendo
com
, eliminamos
e obtemos
Passo 6
Depois, resolvendo
com
, eliminamos
e obtemos
Passo 7
Por fim, resolvendo
com
, chegamos à cláusula vazia
Passo 8
A obtenção da cláusula vazia mostra que o conjunto formado pelas premissas e pela negação da conclusão é insatisfatível.
Resposta
O argumento é válido.