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

Passo 1

O enunciado pede para verificar se, a partir das premissas P Q, Q R, neg R e neg P S, podemos deduzir S. 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 neg S). 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:
C1: P Q equiv neg P lor Q
C2: Q R equiv neg Q lor R
C3: neg R
C4: neg P S equiv P lor S
C5: neg S

Passo 4

Agora aplicamos a resolução entre pares de cláusulas:
Pelo par C2colon neg Q lor R e C3colon neg R, resolvendo em cima de R, obtemos
res1: neg Q

Passo 5

Em seguida, resolvendo C1colon neg P lor Q com neg Q, eliminamos Q e obtemos
res2: neg P

Passo 6

Depois, resolvendo C4colon P lor S com neg P, eliminamos P e obtemos
res3: S

Passo 7

Por fim, resolvendo S com C5colon neg S, chegamos à cláusula vazia
square

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.

Exercícios relacionados