Defina se os argumentos abaixo são válidos com Tableaux. Caso não sejam, mostre o contraexemplo.
Passo 1
O enunciado nos dá as premissas
e pede para verificar se delas decorre
usando o método de Tableaux. Em Tableaux a validade de
é demonstrada mostrando que o conjunto
é insatisfatível (ou seja, o tableau fecha em todos os ramos).
e pede para verificar se delas decorre
usando o método de Tableaux. Em Tableaux a validade de
é demonstrada mostrando que o conjunto
é insatisfatível (ou seja, o tableau fecha em todos os ramos).
Passo 2
Negamos a conclusão e reunimos tudo num único conjunto inicial:
Em seguida aplicamos a regra de desdobramento de conjunção em
, obtendo as fórmulas atômicas
Passo 3
Aplicamos a regra de Tableaux para a implicação
. Isso produz dois ramos, um com
e outro com
:
Ramo 1:
Ramo 2:
Ramo 1:
Ramo 2:
Passo 4
No Ramo 1 temos
mas também já tínhamos
. Logo esse ramo fecha por contradição.
Fica portanto apenas o Ramo 2, que reúne até agora
Fica portanto apenas o Ramo 2, que reúne até agora
Passo 5
Expandimos
em dois subramos: um com
e outro com
.
No subramo fecha-se imediatamente com
.
Segue então o subramo com , que acumula
No subramo
Segue então o subramo com
Passo 6
Expandimos
em
e
.
O ramo fecha com
.
Segue o ramo com , ficando
O ramo
Segue o ramo com
Passo 7
Expandimos
em
e
.
O ramo fecha com
.
Segue então o ramo com , que contém
O ramo
Segue então o ramo com
Passo 8
No ramo atual temos
e
, o que é uma contradição, fechando o último ramo.
Todos os ramos do tableau fecharam, mostrando que
é insatisfatível. Portanto o argumento original é válido.
é insatisfatível. Portanto o argumento original é válido.
Resposta
O argumento é válido.