Verifique a validade dos argumentos, usando tableaux semânticos ou resolução
Passo 1
Vamos verificar o argumento
usando resolução por refutação: precisamos mostrar que assumir a negação da conclusão junto com as premissas gera insatisfatibilidade.
Sabemos que um argumento é válido se
for insatisfatível. Vamos converter cada fórmula em cláusulas (CNF):
Sabemos que um argumento
- A fórmula
já é literal positivo, vira cláusula . -
é equivalente a , cláusula . -
é equivalente a , cláusula .
Passo 2
Adicionamos a negação da conclusão
, ou seja
, como cláusula
. O conjunto completo de cláusulas é:
[{P},{\neg P,\neg Q},{Q,\neg S},{S}]
[{P},{\neg P,\neg Q},{Q,\neg S},{S}]
Passo 3
Agora aplicamos resoluções para chegar à cláusula vazia:
- Resolva
com no literal para obter . - Resolva
com no literal para obter . - Resolva
com no literal para obter a cláusula vazia ( ).
Passo 4
Como chegamos à cláusula vazia, o conjunto de cláusulas é insatisfatível. Logo o argumento original é válido.
Resposta
O argumento é válido.