Verifique a validade dos argumentos, usando tableaux semânticos ou resolução
P, P neg Q, neg Q neg S vdash neg S

Passo 1

Vamos verificar o argumento P,;Ptoneg Q,;neg Qtoneg Svdashneg S 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 Gammavdashalpha é válido se Gammacupnegalpha for insatisfatível. Vamos converter cada fórmula em cláusulas (CNF):
  • A fórmula P já é literal positivo, vira cláusula P.
  • Ptoneg Q é equivalente a neg Plorneg Q, cláusula neg P,neg Q.
  • neg Qtoneg S é equivalente a Qlorneg S, cláusula Q,neg S.

Passo 2

Adicionamos a negação da conclusão neg S, ou seja S, como cláusula S. O conjunto completo de cláusulas é:
[{P},{\neg P,\neg Q},{Q,\neg S},{S}]

Passo 3

Agora aplicamos resoluções para chegar à cláusula vazia:
  • Resolva P com neg P,neg Q no literal P para obter neg Q.
  • Resolva neg Q com Q,neg S no literal Q para obter neg S.
  • Resolva neg S com S no literal S para obter a cláusula vazia ( bot).

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.

Exercícios relacionados